Formal Verification of HotStuff
Chapter
Accepted version
Permanent lenke
https://hdl.handle.net/11250/3054769Utgivelsesdato
2021Metadata
Vis full innførselSamlinger
Originalversjon
Jehl, L. (2021, June). Formal verification of hotstuff. In Formal Techniques for Distributed Objects, Components, and Systems: 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021, Proceedings (pp. 197-204). Cham: Springer International Publishing. 10.1007/978-3-030-78089-0_13Sammendrag
HotStuff is a recent algorithm for repeated distributed consensus used in permissioned blockchains. We present a simplified version of the HotStuff algorithm and verify its safety using both Ivy and the TLA Proof Systems tools.
We show that HotStuff deviates from the traditional view-instance model used in other consensus algorithms and instead follows a novel tree model to solve this fundamental problem. We argue that the tree model results in more complex verification tasks than the traditional view-instance model. Our verification efforts provide initial evidence towards this claim.