2026-07-21T12:58:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13423 2024-03-06T10:31:06Z ddc:004 open_access

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper) Braithwaite, Sean Buchman, Ethan Konnov, Igor Milosevic, Zarko Stoilkovska, Ilina Widder, Josef Zamfir, Anca Blockchain Fault Tolerance Byzantine Faults Model Checking 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sean Braithwaite and Ethan Buchman and Igor Konnov and Zarko Milosevic and Ilina Stoilkovska and Josef Widder and Anca Zamfir 2020 Is Part Of OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FMBC.2020.10 urn:nbn:de:0030-drops-134238 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.10 eng https://creativecommons.org/licenses/by/3.0/legalcode