Presentation

We worked for the formal verification of parts of the L1 of the Tezos blockchain for two grants with the Tezos Foundation of four months each.

The end result is on this website: https://formal-land.gitlab.io/coq-tezos-of-ocaml/ It includes a blog associated with the project describing the technical progress and the challenges we faced, as well as a link to the source code of the project. Everything is open-source under MIT license.