# Is there a way to prove properties about ocaml programs using a Coq verified library
**URL:** https://discourse.rocq-prover.org/t/is-there-a-way-to-prove-properties-about-ocaml-programs-using-a-coq-verified-library/1196
**Category:** Using Rocq
**Created:** [January 21, 2021, 3:57pm UTC](https://discourse.rocq-prover.org/t/is-there-a-way-to-prove-properties-about-ocaml-programs-using-a-coq-verified-library/1196 "2021-01-21T15:57:46Z")
**Posts on this page:** 3
**Page:** 1
### Author:  [@Cjen1](https://discourse.rocq-prover.org/u/Cjen1)
#### Post date: [January 21, 2021, 3:57pm UTC](https://discourse.rocq-prover.org/t/is-there-a-way-to-prove-properties-about-ocaml-programs-using-a-coq-verified-library/1196/1 "2021-01-21T15:57:46Z")
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?
---
### Author:  [@gasche](https://discourse.rocq-prover.org/u/gasche)
#### Post date: [January 24, 2021, 4:13pm UTC](https://discourse.rocq-prover.org/t/is-there-a-way-to-prove-properties-about-ocaml-programs-using-a-coq-verified-library/1196/2 "2021-01-24T16:13:21Z")
I would try using [CFML](https://www.chargueraud.org/softs/cfml/) for this.
---
### Author:  [@mariojppereira](https://discourse.rocq-prover.org/u/mariojppereira)
#### Post date: [January 24, 2021, 9:10pm UTC](https://discourse.rocq-prover.org/t/is-there-a-way-to-prove-properties-about-ocaml-programs-using-a-coq-verified-library/1196/3 "2021-01-24T21:10:50Z")
Let me also add [Cameleer](https://github.com/mariojppereira/cameleer) (which I am currently developing) and [Coq-of-ocaml](https://clarus.github.io/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](https://github.com/ocaml-gospel/gospel) language, and translates it into WhyML (the language of the [Why3](http://why3.lri.fr/) 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](https://vocal.lri.fr/) 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.