Here we give an update on our verification effort on the protocol of Tezos. We add the marks:

• ✅ for "rather done"
• 🌊 for "partially done"
• ❌ for "most is yet to do"

On the website of project, we also automatically generates pages such as Compare to follow the status of the tasks.

Our primary goal at Formal Land 🌲 is to make Tezos the first crypto-currency with a formally verified implementation. With formal verification, thanks to mathematical methods, we can check that a program behaves as expected for all possible inputs. Formal verification goes beyond what testing can do, as testing can only handle a finite amount of cases. That is critical as cryptocurrencies hold a large amount of money (around $3B for Tezos today). The current result of our verification project is available on nomadic-labs.gitlab.io/coq-tezos-of-ocaml. Formal verification is also key to allowing Tezos to evolve constantly in a safe and backward compatible manner.

Recently, we added two new blog posts about the verification of the crypto-currency Tezos:

• Verify the Michelson types of Mi-Cho-Coq to compare the types defined in the Tezos code for the Michelson interpreter and in the Mi-Cho-Coq library to verify smart contracts;
• Translate the Tenderbake's code to Coq to explain how we translated the recent changes in Tezos to the Coq using coq-of-ocaml. In particular we translated the code of the new Tenderbake consensus algorithm.

We also talked at the Lambda Lille Meetup (in French) to present our work on coq-of-ocaml for Tezos. A video on the Youtube channel of the Meetup should be available shortly. We thanks the organizers for hosting the talk.

We added a blog post about the verification of the use of data-encodings in the protocol of Tezos. Currently, we work on the verification of Tezos and publish our blog articles there. We use coq-of-ocaml to translate the OCaml code to Coq and do our verification effort.

Welcome to the blog of Formal Land. Here we will post various updates about the work we are doing.