Document Open Access Logo

Formally Documenting Tenderbake (Short Paper)

Authors Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, Alain Mebsout



PDF
Thumbnail PDF

File

OASIcs.FMBC.2021.4.pdf
  • Filesize: 0.71 MB
  • 9 pages

Document Identifiers

Author Details

Sylvain Conchon
  • Nomadic Labs, Paris, France
Alexandrina Korneva
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France
Çagdas Bozman
  • Functori, Paris, France
Mohamed Iguernlala
  • Functori, Paris, France
Alain Mebsout
  • Functori, Paris, France

Cite AsGet BibTex

Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout. Formally Documenting Tenderbake (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 4:1-4:9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/OASIcs.FMBC.2021.4

Abstract

In this paper, we propose a formal documentation of Tenderbake, the new Tezos consensus algorithm, slated to replace the current Emmy family algorithms. The algorithm is broken down to its essentials and represented as an automaton. The automaton models the various aspects of the algorithm: (i) the individual participant, referred to as a baker, (ii) how bakers communicate over the network (the mempool) and (iii) the overall network the bakers operate in. We also present a TLA+ implementation, which has proven to be useful for reasoning about this automaton and refining our documentation. The main goal of this work is to serve as a formal foundation for extracting intricate test scenarios and verifying invariants that Tenderbake’s implementation should satisfy.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
Keywords
  • Consensus algorithm
  • Tezos blockchain
  • TLA+

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Yackolley Amoussou-Guenou, Antonella Del Pozzo, Maria Potop-Butucaru, and Sara Tucci Piergiovanni. Correctness of tendermint-core blockchains. In 22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China, volume 125 of LIPIcs, pages 16:1-16:16, 2018. Google Scholar
  2. Lăcrămioara Astefănoaei, Pierre Chambart, Antonella Del Pozzo, Thibault Rieutord, Sara Tucci Piergiovanni, and Eugen Zalinescu. Tenderbake - A solution to dynamic repeated consensus for blockchains. In Fourth International Symposium on Foundations and Applications of Blockchain, 2021. Google Scholar
  3. Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir. Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, July 20-21, 2020, Los Angeles, California, USA (Virtual Conference), volume 84 of OASIcs, pages 10:1-10:8, 2020. Google Scholar
  4. Miguel Castro, Barbara Liskov, et al. Practical byzantine fault tolerance. In OSDI, volume 99, pages 173-186, 1999. Google Scholar
  5. LM Goodman. Tezos - A self-amending crypto-ledger white paper. URL: https://www. tezos. com/static/papers/white paper. pdf, 2014. Google Scholar
  6. Jae Kwon and Ethan Buchman. Cosmos whitepaper, 2019. URL: https://cosmos. network/resources/whitepaper.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail