Skip to main content

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

info

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

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, let, match, ...)
  • type definitions
  • monadic programs
  • modules, functors, and first-class modules
  • .ml and .mli files

We also have partial support (with axioms) for:

  • GADTs
  • polymorphic variants
  • extensible types

We are now looking to support the new features introduced in OCaml 5.

Offer

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 contact@formal.land ✉️ 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 🚀