Authors
Longfei Qiu
Jingqi Xiao
Ji-Yong Shin
Zhong Shao
Abstract
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'').
Published
In
Proc. 2026
ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI'26), Boulder, Colorado,
June 2026.
Published as
Proceedings of the ACM on Programming Languages (PACMPL), Volume 10, Number PLDI, Article 215 (June 2026), 26 pages.