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):
- the spending-limit contract,
- several implementations of the FA1.2 token standard, and
- 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.
-
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). ↩
-
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. ↩