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
Publication date
January 2020
DOI Publisher
OASIcs - OpenAccess Series in Informatics. 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) Language
EnglishAbstract
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
Add to ORKG