研究背景与动机
分布式一致性协议（Paxos、Raft、EPaxos等）是构建可靠分布式系统的基础设施。然而，这些协议的正确实现极具挑战性——即使是经过广泛测试的工业级实现（如etcd的Raft实现、Apache Curator的ZooKeeper配方），也曾被发现存在微妙的正确性缺陷。传统的测试方法（单元测试、集成测试、压力测试）难以穷举分布式系统中所有可能的交织执行与故障组合，而Jepsen等故障注入框架虽然能发现部分问题，但缺乏完备性的形式化保证。形式化验证通过数学方法严格证明系统在所有可能执行路径下满足其规约——这正是应对分布式系统复杂性的根本性解决方案。
本项目的核心目标是：开发一套基于TLA+形式化规约的分布式协议验证工具链，为Paxos/Raft/EPaxos等共识算法的实现提供系统性的正确性验证能力，并通过模型检测（Model Checking）在有限状态空间中穷举搜索反例。项目还致力于将形式化方法从学术工具转化为工程实践，通过自动化测试用例生成与CI/CD集成降低形式化验证的使用门槛。
技术栈
- TLA+
- Rust
- Model Checking
- Jepsen
- Chaos Engineering
- TLC
- Apalache
- PlusCal
核心技术贡献
- 多协议形式化规约库 — 使用TLA+编写了Paxos（Basic Paxos与Multi-Paxos）、Raft（Leader Election、Log Replication与Membership Change）、EPaxos（Fast Path与Slow Path）以及CRDT（G-Counter与OR-Set）的完整形式化规约。每个规约包含：常量与变量定义、初始状态、状态转移规则（Next State Relation）、安全性不变式（Safety Invariants）与活性时序属性（Liveness Temporal Properties）。所有规约均通过TLC模型检测器在有限模型下的穷举验证。
- TLA+到Rust的规约驱动测试框架 — 开发了一套将TLA+规约自动转换为Rust测试用例的工具链。核心思路是：TLC模型检测器在执行过程中产生的状态空间轨迹（State Trace）被导出为JSON格式，工具链解析这些轨迹并生成对应的Rust proptest（Property-Based Testing）测试用例。每个测试用例模拟了轨迹中的消息序列与故障事件，并断言实际实现的状态转换与TLA+规约预测一致。
- 混沌工程集成 — 将Jepsen风格的故障注入与TLA+模型检测进行了集成：在Jepsen测试运行期间，实时捕获系统状态（节点角色、日志索引、Leader任期等），将其编码为TLA+状态快照，然后通过TLC验证该快照是否对应规约中的合法状态。这一"在线验证"方法能够在真实分布式环境中发现TLA+规约未覆盖的边界情况。
- 回归测试与社区采纳 — 该框架已在Apache Curator（ZooKeeper客户端库）与etcd（分布式键值存储）的CI流水线中被采纳为回归测试工具。在Curator中，框架发现了一个分布式锁实现中的"羊群效应"（Herd Effect）问题——当锁持有者崩溃时，所有等待者同时尝试获取锁，导致ZooKeeper服务端的瞬时压力激增。该问题在TLA+规约中复现后，通过引入指数退避等待策略得到修复。
- 可视化模型检测器 — 基于TLC的错误轨迹输出，开发了交互式的状态空间可视化工具。该工具以有向图的形式展示模型检测过程中发现的反例路径（Counterexample Trace），每个节点表示一个系统状态，每条边标注触发状态转换的事件。可视化工具显著降低了理解和分析分布式协议边界情况的认知门槛。
工程挑战与解决方案
形式化验证在工程化过程中面临三大核心挑战。第一是状态空间爆炸问题：随着节点数量增加，分布式系统的可达状态数量呈指数级增长——一个5节点的Raft集群在有限模型下可能产生超过10亿个可达状态，这使得穷举模型检测在计算上不可行。我们采用对称性归约（Symmetry Reduction）技术——利用节点角色的对称性将等价的状态合并，将有效状态空间压缩约60%。同时，通过引入归纳不变式（Inductive Invariant）的强化来指导TLC的搜索方向，避免了对不相关状态的无谓探索。
第二是规约与实现之间的语义差距：TLA+规约描述的是协议的数学抽象，而工程实现包含大量实现细节（如网络缓冲区管理、定时器精度、并发锁粒度）。我们通过规约驱动的测试框架来弥合这一差距——从TLC的状态空间轨迹自动生成Rust测试用例，确保实现在每个关键状态转换点上与规约保持一致。第三是开发者接受度：大多数分布式系统开发者对TLA+等形式化工具不熟悉。我们通过开发可视化的模型检测器与交互式的反例浏览器，显著降低了形式化验证的学习曲线与认知门槛。
发现的协议缺陷
Raft Leader Election竞态条件：通过TLA+模型检测发现，在五节点Raft集群中，当网络发生非对称分区（Asymmetric Partition）时，可能出现两个不同任期的Leader同时存在的"脑裂"场景。根本原因在于：Raft的Election Restriction机制仅依赖日志的新旧程度来判断投票资格，未充分考虑网络分区导致的消息延迟。该发现已反馈至Raft论文作者与etcd社区。
Multi-Paxos的Leader Lease安全性：发现Multi-Paxos的Leader Lease优化——即Leader在获得多数派确认后缓存其领导地位——在时钟偏移超过RTT的场景下违反安全性。TLA+模型检测找到了一个具体的反例执行轨迹，验证了Leader Lease必须依赖单调递增的Lease序号（而非依赖时间戳比较）才能保证安全性。