Hi, I’m looking to make things easier for verifying ocaml state machines. With the specific goal of making a ramp into the world of formal verification.
I believe that this to be impossible, but optimally a user could write their state machine using an extracted library in ocaml, and then at a later point start trying to prove things about that state machine.
I think it could be possible via evaluating the state machine to something which could be extracted/transpiled, however I was wondering if there was some easier/less hacky approach to this?
Let me also add Cameleer (which I am currently developing) and Coq-of-ocaml to the options.
The first one can be used to automatically verify OCaml code. It takes an OCaml implementation, annotated with the GOSPEL language, and translates it into WhyML (the language of the Why3 framework). Hence, it allows one to conduct SMT-based verification, which normally means great proof automation. The target of Cameleer are OCaml programs with bounded-mutability (i.e., no heap allocation). Higher-order is restricted to effect-free computations.
The second one takes an OCaml implementation and translates it into Coq. The target of Coq-of-ocaml are purely applicative programs, with support for advanced features such as GADTs or first-class modules.
On a side note, the VOCaL projects aims at building a verified OCaml library of efficient general-purpose data structures and algorithms. Some modules of this library have been extracted from Why3 and Coq proofs.