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.
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).
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