Cameleer

Up until recently, programmers would face a difficult choice if they wished to produce verified OCaml code: either conduct automated proof, but entirely re-implement their code-bases in a proof-aware language, and then rely on code extraction; or verify actual OCaml code, but using an interactive proof assistant, with the burden of manual proofs. Cameleer offers a compromise between the two approaches: it is a tool for the deductive verification of OCaml-written programs, with a clear focus on proof automation. It aims to provide an easy to use framework for the specification and verification of OCaml code.

Cameleer takes as input an OCaml implementation file, annotated using GOSPEL, and translates it into an equivalent WhyML program, the programming and specification language of the [Why3 framework] (https://link.springer.com/chapter/10.1007/978-3-031-71177-0_29#ref-CR14). Why3 is a tool-set for the deductive verification of software, oriented towards automated proof. A distinctive feature of Why3 is that it can interface with different off-the-shelf SMT solvers, which greatly increases proof automation.

With Cameleer, we put forward the vision of the specifying programmer: those who write the code, should also be able to specify it. But, we want to push this vision even further: those who write the code, should be able to specify it and formally verify it. Leveraging on the proof automation and tool-set offered by Why3, we believe Cameleer is a good candidate to fill this need in the working OCaml programmers community.

What inputs are supported?

OCaml, specifications in GOSPEL (Generic Ocaml SPEcification Language).

For which programming languages has it support?

OCaml

What properties can be verified?

What are the tool’s main techniques for the supported (input, property) pairs?

What external tools are used? (e.g., compilers, SMT solvers)

• Why3
• Gospel

What is the tool’s URL?

• https://github.com/ocaml-gospel/cameleer

Example(s)

A comprehensive set of examples is available in the examples folder of the repository.

References

• Mário Pereira, António Ravara
  Cameleer: a Deductive Verification Tool for OCaml
  In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021) DOI

• Mário Pereira
  Practical Deductive Verification of OCaml Programs
  In Proceedings of the 26th International Symposium on Formal Methods (FM 2024) DOI