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.
🐫 Latest blog posts on our formal verification effort on Tezos
· 2 min read