Authors
Longfei Qiu
Jingqi Xiao
Ji-Yong Shin
Zhong Shao
Abstract
Blockchains operating at the global scale demand high-performance
byzantine fault-tolerant (BFT) consensus protocols. Most classic
PBFT-like protocols suffer from an issue known as the leader
bottleneck, which severely limits their throughput and resource
utilization. Recently, Directed Acyclic Graph, or DAG-based protocols,
have emerged as a promising approach for eliminating the leader
bottleneck and achieving better performance. They attain higher
throughput by separating data dissemination and block
ordering. However, their safety and liveness logic is also
significantly more elaborate. So far, most DAG-based protocols have
only enjoyed on-paper security proofs, and it is not clear how to
construct formal proofs of these protocols efficiently.
We introduce LiDO-DAG, a concurrent object model that abstracts the
common logic of these protocols. LiDO-DAG is constructed by combining
a DAG abstraction and LiDO, a recently proposed abstraction for
leader-based consensus. To demonstrate that our framework enables
rapid validation of new DAG-based protocol designs, we implemented
LiDO-DAG in Coq and applied it to three recent DAG-based protocols,
including Narwhal, Bullshark, and Sailfish. Our framework readily
yields mechanized safety and liveness proofs for all three protocols,
which are also the first mechanized liveness proofs of any DAG-based
protocol. Our framework has also revealed an optimization for Sailfish
that improves its worst-case latency.
Published
In
Proc. 2025
ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI'25), Seoul, South Korea,
June 2025.
Published as
Proceedings of the ACM on Programming Languages (PACMPL), Volume 9, Number PLDI, Article 203 (June 2025), 25 pages.