OASIcs.FMBC.2021.4.pdf
- Filesize: 0.71 MB
- 9 pages
Document
Formally Documenting Tenderbake (Short Paper)
Authors
-
Part of:
Volume:
3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-11-30
Cite As Get 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)
0PDF Downloads
References
-
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.
-
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.
-
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.
-
Miguel Castro, Barbara Liskov, et al. Practical byzantine fault tolerance. In OSDI, volume 99, pages 173-186, 1999.
-
LM Goodman. Tezos - A self-amending crypto-ledger white paper. URL: https://www. tezos. com/static/papers/white paper. pdf, 2014.
- Jae Kwon and Ethan Buchman. Cosmos whitepaper, 2019. URL: https://cosmos.network/resources/whitepaper.