一句话：提出 LiDO-DAG 并发对象模型，并在 Coq 中为三种 DAG 共识协议机化验证安全性与活性。
全球规模区块链需要高性能 BFT 共识，但经典 PBFT 类协议受领导者瓶颈限制。基于 DAG 的协议通过分离数据传播与区块排序提升吞吐，却使安全性与活性逻辑更复杂，且多仅有纸面证明。本文提出 LiDO-DAG：结合 DAG 抽象与 LiDO（面向领导者共识的抽象）的并发对象模型，统一刻画此类协议。作者在 Coq 中实现该框架，并应用于 Narwhal、Bullshark 和 Sailfish 三个近期协议，机械化了它们的安全性与活性证明，其中活性证明为 DAG 协议首次。该框架还揭示了 Sailfish 的一项优化，可改善其最坏情况延迟。
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.
@article{paperbot3121,
title = {LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols},
author = {Longfei Qiu and Jingqi Xiao and Ji-Yong Shin and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729306}
}