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. 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?

Cameleer is able to verify functional correctness of an OCaml program, according to a given specification in GOSPEL, including termination.

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

Cameleer translates a given GOSPEL-annotated OCaml program and translates it into an equivalent implementation in WhyML, the programming and specification language of the Why3 tool.

Cameleer can also be used to reason about higher-order functions and control effects with handlers, which are OCaml features missing from the Why3 framework. In such cases, the Cameleer back-end works by translating the mentioned features to WhyML programs that Why3 can handle. In particular, it uses defunctionalization to convert general higher-order functions (with effects) into equivalent first-order implementations. For the case of higher-order iteration functions (e.g., fold_left, iter, etc.), Cameleer provides a custom mechanism that generates a first-order step-by-step cursor that works exactly as the higher-order iterator. The user only provides GOSPEL specification for the higher-order iteration, which is also transformed to fit with the generated cursor (i.e., the user does not even know about the generated first-order implementation). Finally, to reason about control effects handlers, Cameleer features a combination of defunctionalization and clever use of WhyML exceptions to encode such features in WhyML.

At an experimental level, we have recently extended Cameleer to be able to translate selected OCaml programs into the Viper verification language. This allows one to reason about OCaml programs that manipulate dynamic memory.

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

• Why3
• GOSPEL
• Viper

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