Skip to main content

Welcome to the blog

ยท 2 min read
Guillaume Claret

Welcome to the blog of the project "Coq Tezos of OCaml". Here we will report regularly on what we are doing. Our main aims with this project are:

  • to improve the quality of the formalization of Tezos in Coq, and
  • to write as many formal proofs as possible to prevent critical bugs.

Right now we are adding proofs on various pieces of code. We do it in order to have a good coverage in terms of lemma and a good idea of what we are missing. We will do articles about examples of code that we are verifying. We also maintain the formalization of the protocol in sync with the development version in OCaml. To do so, we re-run coq-of-ocaml on the protocol and add the needed changes in a fork.


We believe this project to be a good opportunity for companies or individuals to contribute to the formal verification effort of Tezos. Indeed, it starts from the strong basis of an automatically generated Coq formalization of the protocol, which we maintain over time. This means that a proof has good chances to correspond to what is in the implementation and to become broken if the implementation breaks. To contribute to this project, see the page Contribute.