CFML is a tool for the interactive verification of OCaml programs. It supports programs written in the core language of OCaml, essentially Caml-light plus simple functors. Specifications are expressed as Coq statements, leveraging Separation Logic operators. Proofs are carried out interactively in Coq, using a set of dedicated tactics for stepping through the code line by line, and for providing intermediate specifications such as loop invariants.

CFML has been used to verify, in total, several thousand lines of OCaml, mainly data structure and classic algorithms. Examples include production code, such as the hashtable module from the standard library, and an efficient incremental cycle detection algorithm integrated in the Dune build system.

In this talk, I will give a tour of CFML through the presentation of a few case studies. I will also give an overview of the implementation of CFML2, the new implementation of CFML, briefly describe the CFML extension for amortized asymptotic complexity analysis, and present the plans for the future of CFML.