一句话：提出协议复制数据类型 PRDT，用 RDT 单调累积知识实现共识协议的可组合设计与自动安全验证。
共识协议是分布式系统强一致性的基础，但针对特定用例定制协议易出错，Paxos/Raft 优化变体常需整体重实现，难以复用验证结果。本文提出协议复制数据类型（PRDT）：用 RDT 实现共识协议的编程模型，借鉴基于知识的共识视角，让 RDT 单调累积知识直至达成一致，将协议逻辑与网络细节解耦。作者给出形式模型与证明过程，可自动推理 PRDT 实现的共识安全性，并借助 RDT 代数组合技术构造可组合协议构件。文章在协议的 PRDT 实现中验证适用性并报告性能评估，表明其提升灵活性与可组合性，且无明显性能代价。
Consensus protocols are fundamental in distributed systems as they enable services with strong consistency properties. However, designing protocols optimized for specific use-cases under certain system assumptions is typically an error-prone process requiring expert knowledge. Furthermore, while most recent optimized protocols are variations of well-known algorithms like Paxos or Raft, they often necessitate complete re-implementations, potentially introducing new bugs and complicating the application of existing verification results. This approach impedes application-specific consistency protocols that can easily be amended or swapped out, depending on the given application and deployment scenario. We propose Protocol Replicated Data Types (PRDTs), a novel programming model for implementing consensus protocols using replicated data types (RDTs). Inspired by the knowledge-based view of consensus, PRDTs employ RDTs to monotonically accumulate knowledge until agreement is reached. This approach allows for implementations focusing on high-level protocol logic that abstracts away network details and facilitates automated verification. Moreover, by applying existing algebraic composition techniques for RDTs in the PRDT context, we enable composable protocol building-blocks for implementing complex protocols. We present a formal model of our approach and implement a proof procedure that allows automated reasoning about the consensus safety of concrete PRDT implementations. Additionally, we demonstrate the applicability of our model in verified PRDT-based implementations of existing consensus protocols, and report empirical performance evaluation results. Our findings indicate that the PRDT approach offers enhanced flexibility and composability in protocol design, facilitates reasoning about correctness, and is suited for real-world adoption without intrinsic performance drawbacks.
@article{paperbot12152,
title = {PRDTs: Composable Design and Verification of Consensus Protocols using Replicated Data Types},
author = {Julian Haas and Ragnar Mogk and Annette Bieniusa and Mira Mezini},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839522}
}