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.
- The error monad, internal errors and validity predicates, step-by-step by Pierre Vial: a detailed explanation of what we are doing to verify the absence of unexpected errors in the whole code base;
- Absence of internal errors by Guillaume Claret: the current state of our proofs to verify the absence of unexpected errors;
- Skip-list verification. Using inductive predicates by Bartłomiej Królikowski and Natalie Klaus: a presentation of our verification effort on the skip-list algorithm implementation (part 2);
- Verifying the skip-list by Natalie Klaus and Bartłomiej Królikowski: a presentation of our verification effort on the skip-list algorithm implementation (part 1);
- Verifying json-data-encoding by Tait van Strien: our work to verify an external library used by the Tezos protocol, to safely serialize data to JSON values;
- Fixing reused proofs by Bartłomiej Królikowski: a presentation, with examples, of the work we do to maintain existing proofs and specifications as the code evolves;
- Formal verification of property based tests by Guillaume Claret: the principle and status of our work to formally verify the generalized case of property-based tests;
- Plan for backward compatibility verification by Guillaume Claret: an explanation of the strategy we use to show that two successive versions of the Tezos protocol are fully backward compatible.