Skip to main content

Latest blog posts on our formal verification effort on Tezos

· 2 min read

Here we recall some blog articles that we have written since this summer, on the formal verification of the protocol of Tezos. For this project, we are verifying a code base of around 100,000 lines of OCaml code. We automatically convert the OCaml code to the proof system Coq using the converter coq-of-ocaml. We then apply various proof techniques to make sure that the protocol of Tezos does not contain bugs.

Blog articles 📝

Here is the list of articles about the work we have done since this summer. We believe that some of this work is very unique and specific to Tezos.

To follow more of our activity, feel free to register on our Twitter account 🐦! If you need services or advices to formally verify your code base, you can drop us an email 📧!