The last few weeks have been pretty intense at Nomadic with the preparation of the first community voted upgrade! The team has been working hard on some special future improvements to Tezos…
Improvements to the consensus layer
Tezos has the unique ability to amend itself which allows us to propose state of the art research to the network at any time. This is not a far fetched ideal and will happen sooner rather than later in a series of new efforts spawned at Nomadic dedicated to improving the underlying technology powering the network.
Two of the most prominent paths we are currently exploring relate to consensus.
The first is a refinement of the current protocol, Emmy, by changing the way endorsements are included in a block. This improvement reduces block and endorsement misses, provides expeditious confirmation times and better metrics relating to block confirmation. It is our hope that this particular update will make it into our proposal for the next voting cycle.
The second and more hardcore route is a complete rework of the consensus layer in order to achieve faster finality in a more decisive fashion. We are currently studying the adaptation of classical BFT consensus algorithms to the liquid proof-of-stake system inherent in Tezos.
The Nomadic team is working on a prototype of this new protocol based on Tendermint in collaboration with the French research center (CEA), Cryptium Labs and Arthur Breitman.
Introducing Mi-Cho-Coq
A large subset of the Nomadic Labs team have a strong background in programming language theory and formal verification. Until now most of our efforts have been focused on maturing the node and its infrastructure but this month we have kickstarted a team dedicated solely to formal verification.
Their first product is Mi-Cho-Coq: a framework for the Coq proof assistant to specify Michelson smart contracts and prove properties about them.
Another goal of this effort is to build a repository of simple and idiomatic Michelson contracts for common use cases, with associated proofs. The first one we studied is a multi-signature Michelson contract written by Arthur Breitman. An upcoming post will provide an in-depth review of its proof.
Upcoming in-depth articles
Topics for the next in-depth technical articles include:
- Proving a Multisig contract using Mi-Cho-Coq
- How to Implement Your Own Protocol
- Benchmarking Michelson to Get Accurate Gas Accounting