Nomadic Labs
Nomadic Labs

Introducing Mi-Cho-Coq v1.0

The first public release of the Mi-Cho-Coq framework

It’s our great pleasure to announce Mi-Cho-Coq version 1.0: the first public release of the free and open-source Mi-Cho-Coq framework, a library for verifying the correctness of Michelson smart contract in Coq using weakest-precondition calculus.

The Mi-Cho-Coq framework is a Coq library which models all aspects of the Michelson language: its syntax, its type system, and its semantics.

Although this is the first public release, Mi-Cho-Coq has been in internal use since 2019, including functional verification of some quite large-scale code (some of which is now live):

  1. the spending-limit contract,
  2. several implementations of the FA1.2 token standard, and
  3. several versions of the Dexter decentralized exchange (Dexter v2, Liquidity Baking).

Mi-Cho-Coq also features a simple certified Michelson optimizer1 and it can also be used as a standalone Michelson type checker2

For more details on Mi-Cho-Coq, see the Mi-Cho-Coq README.

  1. A Michelson optimizer is a tool for turning a Michelson script into a semantically equivalent but more efficient one (i.e. it does the same thing, but quicker). Most compilers targeting Michelson come with Michelson optimizers specialized to that compiler’s output. Mi-Cho-Coq’s Michelson optimizer was initially developed for the Albert compiler. For more details about this optimizer, see section 3.3 of our article (see also authors’ pdf). 

  2. So a smart-contract programmer can use Mi-Cho-Coq as a lightweight Michelson smart contract type checker, without having to necessarily run tezos-client