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


Announcing Octez

A veteran implementation of Tezos gets a name: Octez

Rome the city, Rome the ideal There’s a powerful scene in the film the Gladiator where the Emperor Marcus Aurelius explains that Rome is both a physical installation of bricks and mortar, and also it is the idea of Rome — an ecosystem of standards and laws by which the people lived and a city was built. In other words: Rome is a city, and an ideal. When you download Tezos, you are actually downloading code that runs on...

Read More
FA1.2 Approvable Ledger, formal verification by Nomadic Labs

We describe the formal verification in Coq of three FA1.2-compliant smart contracts.

Introduction Overview We’d like to describe a recent verification effort at Nomadic Labs, namely: A formalisation in Coq of the FA1.2 standard; verification in Coq of the formal correctness of three FA1.2 smart contracts with respect to this formalisation; and a description of what we learned from our effort, and of the changes and updates made to the standard and the implementations, following our checks. Background, precise links, and definitions of technical terms1 follow below. Here...

Read More
Five questions to Nomadic Labs PhDs — Guillaume Bau

Short interview with Guillaume Bau, our new PhD student

At Nomadic Labs we are proud to create next-gen software … but we are even prouder to help create the next generation of software scientists! So it’s our great pleasure to host and work with several PhD students, who bring unique perspectives on the technology which they help us to develop, and whose interest in blockchain we are happy to nurture and inform. In this blogpost, we will ask five questions of one of our students, Guillaume...

Read More
Progress report on the verification of Liquidity Baking smart contracts

Context Liquidity baking is one of the main features of the Granada proposal. The feature itself has been well explained by others (initial proposal on Agora, TZIP, Presentation by Midl-dev, Presentation by XTZ.news) so we won’t present it here in details. An original aspect of this feature is that it depends on a smart contract that will likely hold a very high balance. For this reason, the security of this smart...

Read More
Announcing Granada

This is a joint post from Nomadic Labs, Marigold, TQ, Tarides, and DaiLambda. We were proud to see Florence go live on the chain on 11th May 2021. In keeping with our policy of proposing upgrades on a regularly scheduled basis, we’re happy to announce our latest Tezos protocol proposal, Granada. (As is usual, Granada’s “true name” is its hash, which is PtGRANADsDU8R9daYKAgWnQYAJ64omN1o3KMGVCykShA97vQbvV). Granada contains several major improvements to the protocol, as well as...

Read More
Simulating Tenderbake

Announcing a simulator for Tenderbake

If you’re impatient, you are welcome to read the guide and jump right to the simulator now. See also the implemented algorithms below. If you find that reading about it helps you get excited before using your simulator, then read on … Background The consensus algorithm is a crucial part of any blockchain project. Because of the distributed nature of blockchains, different nodes can have different ideas of what the current state of the blockchain is supposed to be....

Read More
Five questions to Nomadic Labs PhDs — Colin Gonzalez

Short interview with Colin Gonzalez, our new PhD student

At Nomadic Labs we are proud to create next-gen software … but we are even prouder to help create the next generation of software scientists! So it’s our great pleasure to host and work with several PhD students, who bring unique perspectives on the technology which they help us to develop, and whose interest in blockchain we are happy to nurture and inform. In this blogpost, we will ask five questions of one of our students, Colin...

Read More
Faster finality with Emmy*

Announcing forthcoming upgrade of consensus protocol, giving quicker time to finality (i.e. shorter transaction settlement times)

We are happy to announce that Emmy* is set to be included in the next Tezos protocol proposal Granada,1 replacing the current consensus algorithm Emmy+. If Granada is adopted, Emmy* will generally halve the time between blocks, from 60 seconds to 30 seconds, and allow transactions to achieve significantly faster finality than under the current consensus algorithm, Emmy+. Specifically, Emmy* updates Emmy+ by: a tweak in the definition of the minimal delay function, and an increase in...

Read More
Announcing the report “Possible evolutions of the voting system in Tezos”

Announcing a report on possible evolutions of the voting system in Tezos

Nomadic labs has an ongoing research relationship with INRIA (a French national technology research agency). In the context of this relationship, Nomadic Labs commissioned a short report to explore what a privacy-preserving amendment procedure might look like on Tezos, authored by three experts in voting protocols and cryptography: Véronique Cortier, Pierrick Gaudry and Stéphane Glondu. There is no plan to implement the contents of the report for now, but we welcome and...

Read More