一句话：提出 SureDistrib 形式化框架，支持概率安全/活性规范与精化组合，并首次机器化证明异步拜占庭二元共识几乎必然终止。
异步共识协议不依赖有界延迟来维持活性，但由于 FLP 不可能性只能提供概率活性保证，且通常由多层算法组合而成，其正确性尤其是活性极难验证，已有协议存在多年未被发现的活性缺陷。本文提出 SureDistrib，一个用于规范和验证异步分布式协议概率安全性与活性属性的形式化框架。该框架支持规范依赖其他概率功能性的概率算法，例如依赖 common coin 的二元一致性算法；作者定义此类系统的精化关系，并证明组合引理，从而可用具体实现替换底层抽象功能性，使复合系统精化原抽象底层系统。基于该框架，作者给出了首个机器化证明：异步拜占庭容错二元一致性算法以概率 1 终止，即几乎必然终止。
Consensus algorithms play a central role in many distributed systems, including blockchains. The most practical consensus algorithms are based on the partial synchrony model. While partially synchronous protocols are relatively simple, they cannot maintain liveness when the message delivery latency is uncertain. Asynchronous protocols do not rely on bounded latency to maintain liveness, but they are much more difficult to understand and implement, being usually described as a composition of several layers of algorithms. Moreover, due to the FLP impossibility theorem, they only provide probabilistic liveness guarantees. These factors make the correctness of asynchronous protocols challenging to verify, and there have been liveness bugs in these protocols that remain unnoticed for years. We introduce SureDistrib, a formal framework for specifying and verifying probabilistic safety and liveness properties of asynchronous distributed protocols. Our framework supports specifying probabilistic algorithms that depend on other probabilistic functionalities, such as binary agreement algorithms depending on common coins. We define refinement relations for such systems, and prove composition lemmas that replace the underlay functionality with an implementation, so that the composed system refines the original system with an abstract underlay. Based on our framework, we give the first mechanized proof that an asynchronous byzantine fault-tolerant binary agreement algorithm terminates with probability 1 ("almost-sure termination").
@article{QiuXSS26,
title = {SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols},
author = {Longfei Qiu and Jingqi Xiao and Ji-Yong Shin and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808293}
}