一句话：提出结合鞅与弱公平性的可靠证明规则，在 Caesar 上以 SMT 验证随机分布式共识的几乎必然终止。
本文研究随机化分布式算法活性性质（几乎必然终止）的验证问题。作者提出一条可靠的证明规则，将基于鞅（martingale）的几乎必然终止技术与弱公平性推理相结合，并能处理状态无界增长的参数化协议，突破了此前依赖有界变体函数或归约到非概率公平性的限制。该规则在概率程序验证器 Caesar 上实现，可生成 SMT 证明。作者用其对随机异步共识协议（包括 Ben-Or 协议与 graded binary consensus）在崩溃故障与拜占庭故障下的终止性给出证明；这些协议的终止性证明历来困难，此前方法无法覆盖。
We present a technique for the verification of liveness properties of randomized distributed algorithms. Our technique gives SMT-based proofs for many common consensus algorithms, both for crash faults and for Byzantine faults. It is based on a sound proof rule for fair almost-sure termination of distributed systems that combines martingale-based techniques for almost-sure termination with reasoning about weak fairness. Our proof rule is able to handle parametrized protocols where the state grows unboundedly and every variant function is unbounded. These protocols were out of scope for previous approaches, which either relied on bounded variant functions or on reductions to (non-probabilistic) fairness. We have implemented our proof rules on top of Caesar, a program verifier for probabilistic programs. We use our proof rule to give SMT-based proofs for termination properties of randomized asynchronous consensus protocols, including Ben-Or’s protocol and graded binary consensus, for both crash and Byzantine faults. These protocols have notoriously difficult proofs of termination but fall within the scope of our proof rule.
@article{EneaMMS26,
title = {Verifying Almost-Sure Termination for Randomized Distributed Algorithms},
author = {Constantin Enea and Rupak Majumdar and Harshit Jitendra Motwani and V. R. Sathiyanarayana},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776691}
}