License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2021.4
URN: urn:nbn:de:0030-drops-154281
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15428/
Go to the corresponding OASIcs Volume Portal

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

Formally Documenting Tenderbake (Short Paper)

pdf-format:
OASIcs-FMBC-2021-4.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{conchon_et_al:OASIcs.FMBC.2021.4,
  author =	{Conchon, Sylvain and Korneva, Alexandrina and Bozman, \c{C}agdas and Iguernlala, Mohamed and Mebsout, Alain},
  title =	{{Formally Documenting Tenderbake}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{4:1--4:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/15428},
  URN =		{urn:nbn:de:0030-drops-154281},
  doi =		{10.4230/OASIcs.FMBC.2021.4},
  annote =	{Keywords: Consensus algorithm, Tezos blockchain, TLA+}
}

Keywords: Consensus algorithm, Tezos blockchain, TLA+
Collection: 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
Issue Date: 2021
Date of publication: 30.11.2021
Supplementary Material: Model (Source Code): https://www.lri.fr/~conchon/tenderbake/Tenderbake.tla

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI