CFML is a tool for the interactive verification of OCaml programs, using Coq and Separation Logic. The source files can be obtained from: git clone git@github.com:charguer/cfml.git For installation instruction, read the README file.The developments rely on my Coq library TLC.All the files are distributed under the GNU-LGPL license.