Document Open Access Logo

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)

Authors Sean Braithwaite, Ethan Buchman, Igor Konnov , Zarko Milosevic , Ilina Stoilkovska, Josef Widder , Anca Zamfir

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2020.10.pdf
  • Filesize: 0.5 MB
  • 8 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Software and its engineering → Software fault tolerance
  • Theory of computation → Logic and verification
Keywords
  • Blockchain
  • Fault Tolerance
  • Byzantine Faults
  • Model Checking

Metrics

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

Abstract

Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them.

Cite As Get BibTex

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 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 10:1-10:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.FMBC.2020.10

Author Details

Sean Braithwaite
  • Informal Systems, Lausanne, Switzerland
Ethan Buchman
  • Informal Systems, Toronto, Canada
Igor Konnov
  • Informal Systems, Wien, Austria
Zarko Milosevic
  • Informal Systems, Lausanne, Switzerland
Ilina Stoilkovska
  • Informal Systems, Wien, Austria
Josef Widder
  • Informal Systems, Wien, Austria
Anca Zamfir
  • Informal Systems, Lausanne, Switzerland

Funding

Supported by Interchain Foundation (Switzerland).

Supplementary Materials

References

  1. APALACHE: a symbolic model checker for TLAsuperscript+. https://github.com/konnov/apalache/, 2020. Last accessed: May 20, 2020.
  2. Ethan Buchman. Tendermint: Byzantine fault tolerance in the age of Blockchains. Master’s thesis, University of Guelph, 2016. URL: http://hdl.handle.net/10214/9769.
  3. Ethan Buchman and Jae Kwon. Cosmos whitepaper: a network of distributed ledgers, 2016. URL: https://cosmos.network/resources/whitepaper.
  4. Ethan Buchman, Jae Kwon, and Zarko Milosevic. The latest gossip on BFT consensus. arXiv preprint arXiv:1807.04938, 2018. URL: https://arxiv.org/abs/1807.04938.
  5. Vitalik Buterin and Virgil Griffith. Casper the friendly finality gadget. arXiv preprint arXiv:1710.09437, 2017. Google Scholar
  6. Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. J.ACM, 35(2):288-323, 1988. Google Scholar
  7. Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. TLA+ model checking made symbolic. PACMPL, 3(OOPSLA):123:1-123:30, 2019. Google Scholar
  8. Markus Alexander Kuppe, Leslie Lamport, and Daniel Ricketts. The TLA+ toolbox. In F-IDE@FM 2019, pages 50-62, 2019. Google Scholar
  9. Jae Kwon. Tendermint: Consensus without mining. Draft v. 0.6, fall, 1(11), 2014. Google Scholar
  10. Informal Systems. Fastsync - English specification, 2020. URL: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/fastsync/fastsync.md.
  11. Informal Systems. Fastsync - TLA^+ specification, 2020. URL: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/fastsync/fastsync.tla.
  12. Informal Systems. Verification-Driven Development: An Informal Guide, 2020. URL: https://github.com/informalsystems/VDD/blob/master/guide/guide.md.
  13. ADR 043: Blockhchain reactor riri-org, 2020. URL: https://github.com/tendermint/tendermint/blob/master/docs/architecture/adr-043-blockchain-riri-org.md.
  14. Tendermint core, reference implementation in Go, 2020. URL: https://github.com/tendermint/tendermint.
  15. Maofan Yin, Dahlia Malkhi, Michael K Reiter, Guy Golan Gueta, and Ittai Abraham. Hotstuff: BFT consensus with linearity and responsiveness. In PODC, pages 347-356, 2019. Google Scholar
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact