A Toolchain for Verified OCaml Programs

This paper presents a methodology to verify OCaml programs with respect to behavioral specifications, using the Why3 tool. First, a formal specification is given in the form of an OCaml module signature extended with type invariants and function contracts, in the spirit of JML. Second, an implementation is written in the programming language of Why3 and then verified with respect to the specification. Finally, an OCaml program is obtained by an automated translation. This methodology is illustrated on several idiomatic OCaml programs. We discuss some of the challenges, such as proving the absence of arithmetic overflows, checking preconditions at runtime, and verifying stateful higher-order functions.