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.