🐫 OCaml verification
To formally verify OCaml programs we are developing the translator coq-of-ocaml. It translates OCaml code to similar-looking code in the interactive proof assistant Coq. We are then expert in the Coq system and can formally verify arbitrarily complex properties.
Our leading application is the project Coq Tezos of OCaml, where we are formally verifying a codebase of around 100,000 lines of OCaml for the crypto-currency Tezos ꜩ. To this day, we have written around 60,000 lines of Coq code, and are verifying:
- the absence of internal errors,
- the backward compatibility,
- the preservation of the invariants,
- the serialization functions.
As an example,
coq-of-ocaml translates the following OCaml code:
(* OCaml code *)
let rec sum tree =
match tree with
| Leaf n -> n
| Node (tree1, tree2) -> sum tree1 + sum tree2
to the corresponding Coq code:
(* Coq code generated by `coq-of-ocaml` *)
Fixpoint sum (tree : tree int) : int :=
match tree with
| Leaf n => n
| Node tree1 tree2 => sum tree1 +i sum tree2
As you can see, there are no much differences between the two apart from the syntax. For example, we try to never generate new variable names during the translation. Having a Coq code that is similar in shape and in size to the original program helps us to write formal proofs more efficiently. Following an existing codebase is also a good idea to organize all the proofs when certifying a software.
We support a large subset of OCaml, including:
- the functional core (functions,
- type definitions
- monadic programs
- modules, functors, and first-class modules
We also have partial support (with axioms) for:
- polymorphic variants
- extensible types
We are now looking to support the new features introduced in OCaml 5.
If you want to make extra secure OCaml programs (to be applied in domains such as aviation, automotive, or medical devices) with formal verification, you can contact us by email at firstname.lastname@example.org ✉️ or schedule a call on koalendar.com/e/meet-with-formal-land ☎️. Our main expertise is in the Coq system. We estimate there should be one Coq developer for each three or four OCaml developers to make formally verified software.
Helping you build 🚀