Introducing Mi-Cho-Coq v1.0
The first public release of the Mi-Cho-Coq framework
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...
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...
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...
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...
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...
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....
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...
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...
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...