Mi-Cho-Coq is a Coq framework which we use to verify smart contracts written in Michelson, the language of smart contracts for Tezos. You can get an introduction to formal verification on Michelson code on opentezos.com/formal-verification.

We want the highest possible level of confidence in the result of our verification work but there is a gap between Mi-Cho-Coq, which was manually written in Coq, and the Tezos protocol. To fill this gap, we want to prove that the semantics of the Michelson language defined in Mi-Cho-Coq exactly matches the mechanic translation of the Michelson interpreter from the Tezos protocol, which we import to Coq using coq-of-ocaml. Defining a bijection between the two type grammars is a requirement for this project. A difficulty is that, because Michelson evolves quickly and Mi-Cho-Coq is handwritten, some recent features are missing in Mi-Cho-Coq. This verification work can also help in identifying them.