Since Michael O'Church mentioned it, I decided to do a quick search on any practical uses of Ocaml that overlapped with formal verification. This was first, good find. The tool appears to improve on expression, correctness analysis, and testing. Also supports incremental verification of primitives in provers aka “pay as you go” correctness. Compilation verification is also relatively straight-forward per Esterel SCADE report due to good, compiler design.