Here are some interesting projects that use Coq proofs, I'll leave it up to you to judge how real world they are. Generate OCaml code from Coq: https://github.

Here are some interesting projects that use Coq proofs, I'll leave it up to you to judge how real world they are. Generate OCaml code from Coq: https://github.com/msgpack/msgpack-ocaml/tree/master/proof https://github.com/msgpack/msgpack-ocaml/tree/master/proof Proof algorithms written in OCaml using Coq: http://www.chargueraud.org/softs/cfml/ http://www.chargueraud.org/softs/cfml/ Write program specification and use multiple provers (including Coq): http://why3.lri.fr/ http://why3.lri.fr/ Write certified programs, and verify proofs using Coq: http://focalize.inria.fr/ http://focalize.inria.fr/ Language semantics / type system proofs of languages: http://www.cl.cam.ac.uk/~so294/ocaml/ http://www.cl.cam.ac.uk/~so294/ocaml/ (for a subset of OCaml) http://gallium.inria.fr/~protzenk/mezzo-lang/ http://gallium.inria.fr/~protzenk/mezzo-lang/ Books on Coq: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/