Skip to main content



A translation in Coq of the economic protocol. We list here all the Coq code generated from the implementation written in OCaml. We use the tool coq-of-ocaml to automatically generate the Coq code from the OCaml files.

The generated Coq code should be similar to the original OCaml code. In each file, there is a link to access the original OCaml code in order to compare the two. There is also a link to a corresponding proofs file, when there is one. The proofs file contains the specifications and formal verification of associated properties.

For some of the files which are too complex to translate to Coq, we instead translate their corresponding interface (.mli) files. The translation of an interface file is a Coq file suffixed by _mli.v. When some individual functions are too complex to translate, we annotate them in the source code and generate a Coq axiom.