论文标题
在AGDA中正式验证基于热的拜占庭式容错共识：扩展版本
Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version
论文作者
论文摘要
LibrAbft是基于HotStuff的拜占庭式容错（BFT）共识协议。我们提出了Hotstuff / librabft基础协议的抽象模型，以及正式的，由机器检查的核心正确性（安全性）属性的证据，以及一个扩展条件，使无参与方验证承诺的结果。 （将证明具有特定实现的属性属性，而不是本文介绍的摘要模型。） 一个关键的贡献是精确地定义了关于诚实同龄人的行为的假设，该假设与任何特定的实现无关。因此，我们的工作是证明整个混凝土实现的正确性的重要一步，而无需重复证明基本协议正确性的辛勤工作。抽象证明是用于单个配置（Epoch）；将这些证据跨在配置更改中扩展是未来的工作。我们的模型和证明在AGDA中表达，并在开源中提供。
LibraBFT is a Byzantine Fault Tolerant (BFT) consensus protocol based on HotStuff. We present an abstract model of the protocol underlying HotStuff / LibraBFT, and formal, machine-checked proofs of their core correctness (safety) property and an extended condition that enables non-participating parties to verify committed results. (Liveness properties would be proved for specific implementations, not for the abstract model presented in this paper.) A key contribution is precisely defining assumptions about the behavior of honest peers, in an abstract way, independent of any particular implementation. Therefore, our work is an important step towards proving correctness of an entire class of concrete implementations, without repeating the hard work of proving correctness of the underlying protocol. The abstract proofs are for a single configuration (epoch); extending these proofs across configuration changes is future work. Our models and proofs are expressed in Agda, and are available in open source.
