# Coq translation of the Tezos protocol

**URL:** https://discourse.rocq-prover.org/t/coq-translation-of-the-tezos-protocol/1412
**Category:** Announcements
**Created:** [August 11, 2021, 6:08pm UTC](https://discourse.rocq-prover.org/t/coq-translation-of-the-tezos-protocol/1412 "2021-08-11T18:08:18Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![clarus](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/clarus/32/237_2.png) [@clarus](https://discourse.rocq-prover.org/u/clarus)
#### Post date: [August 11, 2021, 6:08pm UTC](https://discourse.rocq-prover.org/t/coq-translation-of-the-tezos-protocol/1412/1 "2021-08-11T18:08:18Z")

</div>

A post to present the [coq-tezos-of-ocaml](https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/) project, aiming to help verify the crypto-currency [Tezos](https://tezos.com/). This project contains a translation in Coq of the [economic protocol](https://gitlab.com/tezos/tezos/-/tree/master/src/proto_alpha/lib_protocol) written in OCaml. We generate this translation using [coq-of-ocaml](https://clarus.github.io/coq-of-ocaml/). The translation is a shallow embedding of OCaml in Coq, expecting the side-effects to be into monads (mainly the state and errors effects for Tezos).

There are about 40.000 lines of generated Coq code, for around 30.000 lines of OCaml code as input. We write proofs on the translation in order to look for bugs. This matters as Tezos is a decentralized network, so a bug would allow stealing a large amount of money with minimal legal risks. Most of the proof work is yet to be done. Among things we want to verify are:

- the equivalence between the Michelson interpreter and the [Mi-Cho-Coq](https://gitlab.com/nomadic-labs/mi-cho-coq) specification used to verify smart-contracts (the initial goal of the project);
- the validity of the [storage](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/storage.ml) system, showing it can be simulated by standard OCaml data-structures;
- all possible code invariants which would otherwise be verified by unit-testing.

An example of code translation to Coq from the protocol is the following:

```ocaml
(* input in amendment.ml *)
let may_start_new_voting_period ctxt =
  Voting_period.is_last_block ctxt >>=? fun is_last ->
  if is_last then start_new_voting_period ctxt else return ctxt

```

```coq
(* output in Amendment.v *)
Definition may_start_new_voting_period (ctxt : Alpha_context.context)
  : M=? Alpha_context.context :=
  let=? is_last := Alpha_context.Voting_period.is_last_block ctxt in
  if is_last then
    start_new_voting_period ctxt
  else
    return=? ctxt.

```

Contributions are welcomed, especially to write new proofs. For that, you can look at the [contribute page](https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/contribute/).