Definition of the Michelson interpreter using dependent types instead of GADTs.
Definition of the Michelson type-checker and parser using dependent types instead of GADTs.
Verification of the backward compatibility of the interpreter between the protocols J and K.
We present a translation and verification in the Coq language of the source code of the economic protocol of Tezos. The Coq language is a formal language used to write mathematical reasoning, such as theorems and proofs, and verify their correctness. We use this translation to Coq to formally verify the absence of certain classes of bugs in all possible execution scenarios. We use the tool coq-of-ocaml to automatically generate this translation from the implementation.
We also show our formalization of the environment interface of the protocol given in the tezos/tezos node. This environment interface is the set of functions of values that the protocol can call. It is a subset of the standard library of OCaml and is specified as a module signature. We axiomatize or define each of its functions and values in Coq.
Together with this project, there are other initiatives to do formal verification on Tezos. This includes Mi-Cho-Coq to formally verify smart contracts and a project in development at Nomadic Labs for a high-level certification of the protocol.