一句话：将强复制系统作为弱复制数据存储的应用，并用 Super-V 以局部稳定更新前置条件实现基于 SMT 的共识安全验证。
强一致复制数据存储是许多在线服务的基础，但其实现复杂：网络分区下不可用，容错需正确实现 Raft/Paxos 等共识算法。这些算法难以推理，现有分布式共识验证工具因异步消息传递的低层模型而需要过多人工投入。本文将强复制系统视为弱复制数据存储的应用：弱存储在分区下仍可用，能抽象异步通信，并导出验证共识安全性的局部作用域条件。作者开发了弱复制状态模型的验证编程框架 Super-V，以稳定更新前置条件替代全局归纳不变式，实现基于 SMT 的自动验证。评估中，他们实现并验证了一个改造自 Raft 的强复制系统。
Strongly-consistent replicated data stores are a popular foundation for many kinds of online services, but their implementations are very complex. Strong replication is not available under network partitions, and so achieving a functional degree of fault-tolerance requires correctly implementing consensus algorithms like Raft and Paxos. These algorithms are notoriously difficult to reason about, and many data stores implement custom variations to support unique performance tradeoffs, presenting an opportunity for automated verification tools. Unfortunately, existing tools that have been applied to distributed consensus demand too much developer effort, a problem stemming from the low-level programming model in which consensus and strong replication are implemented—asynchronous message passing—which thwarts decidable automation by exposing the details of asynchronous communication. In this paper, we consider the implementation and automated verification of strong replication systems as applications of weak replicated data stores. Weak stores, being available under partition, are a suitable foundation for performant distributed applications. Crucially, they abstract asynchronous communication and allow us to derive local-scope conditions for the verification of consensus safety. To evaluate this approach, we have developed a verified-programming framework for the weak replicated state model, called Super-V. This framework enables SMT-based verification based on local-scope artifacts called stable update preconditions, replacing standard-practice global inductive invariants. We have used our approach to implement and verify a strong replication system based on an adaptation of the Raft consensus algorithm.
@article{paperbot3157,
title = {Bolt-On Strong Consistency: Specification, Implementation, and Verification},
author = {Nicholas V. Lewchenko and Gowtham Kaki and Bor-Yuh Evan Chang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720502}
}