Skip to main content



A formalization of the primitives used by the protocol, as taken from the tezos/tezos node. These primitives include for example:

  • elements from the standard library of OCaml (numbers, lists, maps, ...);
  • cryptographic primitives;
  • serialization primitives (library of data-encoding).

We write the formalization of the environment mostly by hand, verifying that it corresponds to what is in the implementation. We do so by checking that the signatures of the definitions are compatible with what coq-of-ocaml generates in src/Proto_alpha/Environment.v, using module signature inclusion.