Skip to main content

· 8 min read

In the protocol of Tezos, we define the serialization of values using the data-encoding library. We make these definitions by hand to be able to audit the code and fine-tune the serialization.

The serialization and deserialization functions must be inverse. Missing this property can lead to bugs or exploits. We present a solution to formally verify the definition of data-encodings in Coq. As a result, we increase our confidence in the correctness of our encodings. We even found a mistake in a development code and fixed it before release. This mistake was found by TriliTech.

· 5 min read

An issue with recursive functions is that they may raise a stack-overflow error if the number of recursive calls is too high. To avoid these errors, many functions in Tezos are written in tail-recursive style. This style is usually harder to read and this could lead to mistakes in the code. We show in this post how we verify a tail-recursive function by comparing it to its naive non tail-recursive version.

· 2 min read

Welcome to the blog of the project "Coq Tezos of OCaml". Here we will report regularly on what we are doing. Our main aims with this project are:

  • to improve the quality of the formalization of Tezos in Coq, and
  • to write as many formal proofs as possible to prevent critical bugs.