一句话：提出 AdoB 抽象，统一建模良性/拜占庭共识，并在 Coq 中机械验证安全性与活性。
分布式共识在良性故障与拜占庭故障下都极具挑战，但此前缺乏能统一支持二者机械验证的合适抽象。本文基于原子分布式对象模型提出 AdoB，用同一套抽象表示良性及拜占庭共识，避免细节丢失与模型过度复杂。作者在 Coq 中证明了 AdoB 的安全性与活性，这是首个统一处理两类共识的机械化证明；并证明标准网络层规约的 Fast Paxos 与 Jolteon 变体可精化 AdoB，说明该抽象能忠实建模真实协议，同时降低分布式系统验证难度。
Achieving consensus is a challenging and ubiquitous problem in distributed systems that is only made harder by the introduction of malicious byzantine servers. While significant effort has been devoted to the benign and byzantine failure models individually, no prior work has considered the mechanized verification of both in a generic way. We claim this is due to the lack of an appropriate abstraction that is capable of representing both benign and byzantine consensus without either losing too much detail or becoming impractically complex. We build on recent work on the atomic distributed object model to fill this void with a novel abstraction called AdoB. In addition to revealing important insights into the essence of consensus, this abstraction has practical benefits for easing distributed system verification. As a case study, we proved safety and liveness properties for AdoB in Coq, which are the first such mechanized proofs to handle benign and byzantine consensus in a unified manner. We also demonstrate that AdoB faithfully models real consensus protocols by proving it is refined by standard network-level specifications of Fast Paxos and a variant of Jolteon.
@article{paperbot2543,
title = {AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects},
author = {Wolf Honoré and Longfei Qiu and Yoonseung Kim and Ji-Yong Shin and Jieung Kim and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649826}
}