The main work needed is to write proofs.
In this project, we present a translation in Coq of the implementation of the economic protocol of Tezos. This translation by itself does not provide any additional safety. It is only useful if we can verify properties on this translation. Since we translate OCaml code to vanilla Coq code, it should be possible to verify arbitrarily complex properties given the right lemmas.
We believe that this project represents a unique opportunity to write interesting Coq proofs, as:
- there is a lot of code to verify (around 50.000 lines);
- this is about a real implementation with a lot of money at stake (Tezos);
- the code is mostly purely functional or monadic (high-level, no low-level issues like pointers analysis, few encodings);
- this is updated as the OCaml source code changes. So the aim is also to write maintainable proofs, interacting with the OCaml developers.
If you want to start writing proofs about the protocol and want to communicate about that, please either:
- open an issue with what you want to prove on coq-tezos-of-ocaml/-/issues;
- go on the #coq-tezos-of-ocaml channel for those who are the
- write an email to
To make a contribution, open a merge request on coq-tezos-of-ocaml/-/merge_requests.
The code is in the GitLab repository coq-tezos-of-ocaml, with the latest protocol version in the folder src/Proto_alpha/. Since the protocol structure is flat (all the files in the same folder), the Coq translation is also flat. The translated files have the same name as in OCaml but are capitalized to follow the Coq's convention. For example,
apply.ml is translated to
We translate the
.mli file of the environment in
Environment.v. Because this is a
.mli file, we generate a translation with one Coq axiom per declaration in OCaml. In the folder
Environment/, we have one file per module of the environment. These files are written by hand. They contain the concrete definitions or the axiomatized specifications of the environment. We check, by module inclusion, that the definitions in the
Environment/ folder are compatible with the declarations in the
We put our proofs files in
Proofs/ folders, using the same name as the file they are referring to. For example, the proofs about the
Apply.v file would be put into
Proofs/Apply.v. We also have a folder
Environment/Proofs/ for the definitions of the environment in
Environment/. This follows the convention used by some projects of putting test files in a
test/ folder, with the same name as the tested file.
.ml files which would be too hard to translate to Coq, we translate the corresponding
.mli file to axioms. Otherwise, we only translate the
Here are a few examples to start contributing to the formal verification of the protocol of Tezos:
- having lemmas about the Environment/Map.v and Environment/_Set.v data structures;
- filling up definitions for parts of the environment that are axioms but could be replaced by definitions. For example, in Environment/List.v, there are still many primitives declared as
Parameter, which should be replaced by a corresponding
Definition. Having the usual lemmas about the list primitives could be useful too.
- verifying properties about files without too many dependencies, like for example Misc.v;
- verifying properties about high-level files, like Apply.v, using axioms about what is needed when there are calls to other files.
Also, we are currently verifying the storage of the protocol, what should help to reason about functions using the storage. A function may use the storage when it is parametrized by the context
ctxt. This is an inlined state monad.
To see how to re-generate the Coq translation of the protocol, look at this HOWTO document. This can be useful to understand how the translation works or to update the OCaml source to simplify the proofs.