你无法对分布式协议做单元测试。单元测试在一台机器上以一个顺序运行一个进程。而你的协议在五台机器上以十个进程、以你无法控制的顺序运行。这两种现实之间的鸿沟，正是缺陷藏身之处。

模型检验弥合了这一鸿沟。它穷举协议可能到达的每一种状态的所有可能交错。如果存在两条副本不一致的路径、存在领导者选举陷入死锁的路径、或存在 split-brain 出现的路径，模型检验器都会发现它。而且是在你写下第一个 RPC handler 之前就发现。

为什么分布式缺陷能躲过传统测试

问题出在状态爆炸。三个节点交换消息就可能产生数十亿条执行路径。手写的集成测试也许只能覆盖其中十几条，通常是 happy path 和少数几个明显的故障模式。节点 A 恰好在发送 prepare 和 ack 之间崩溃的缺陷？祝你在 CI 里碰上它。

形式化验证听起来像是学术练习，但模型检验不同。你并非要证明协议永远正确。你用规约语言描述协议，定义你关心的性质，然后让工具在某一界限内穷举状态空间。一旦发现违反，它会给出最小反例追踪。你会得到一份逐步复现缺陷的配方。没有 heisenbugs，没有“在我机器上能跑”。

最实用的工具是 Leslie Lamport 开发的 TLA+。它看起来像数学，因为它就是数学。但数学比你想的简单，回报则是找到那些否则会在凌晨两点于生产环境爆发的缺陷。

模型检验到底在做什么

模型检验器接收三个输入：系统描述、环境描述、以及你希望保持的性质。系统描述捕获协议逻辑。环境描述捕获你无法控制的一切：网络延迟、消息丢失、节点崩溃、时钟偏移。性质通常是不变式（“已提交的日志永不被覆盖”）或活性条件（“每个请求最终都会得到响应”）。

然后检验器生成每一个可达状态以及状态之间的每一个合法转移。对有限状态空间它彻底穷举，对无限空间则做有界探索。若不变式被违反，它停止并报告到达失败的最短路径。

这是暴力枚举，不是魔法。模型检验器不理解你的意图。它只是尝试一切。这正是关键所在。你的集成测试受你的假设左右。模型检验器没有假设。

在 TLA+ 中规约一个简单的共识协议

来看一个最小示例：一个单法令共识协议，领导者提出一个值，接受者的法定人数必须在值被选定前接受它。这是 Paxos、Raft 以及你听过的所有其他共识算法的核心思想。

以下是该系统的 TLA+ 规约：

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

这份规约说明：最初没有任何值被选定。一个 propose 动作可以将 chosen 设为单个值，但前提是目前还没有任何值被选定。ChosenUniqueness 不变式规定，任何时候被选定的值至多只有一个。

TLA+ 的模型检验器 TLC 会验证没有任何执行追踪违反 ChosenUniqueness。如果你引入一个缺陷，让两个领导者可以在不检查已有值的情况下同时提出，TLC 会在数毫秒内找到反例。

加入混乱的部分：崩溃与消息丢失

上面的规约太干净了。真正的分布式系统并不干净。消息会丢失。节点会重启。网络分区会把一群节点彼此隔离。只有当你把这些故障也建模进来，模型才有用。

下面是一个更贴近现实的片段，对可能发生丢失的消息传递进行建模：

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop 是重要的补充。它在不改变接受者状态的情况下建模消息丢失。TLC 会探索任何消息被投递、被丢弃或被无限期延迟的追踪。当你加入领导者崩溃与恢复后，状态空间会增长，但 TLC 仍会系统性地探索它。

这是我刚开始接触 TLA+ 时被绊倒的地方。我只想建模协议逻辑。但缺陷不在逻辑里。它们藏在我没有考虑到的逻辑与故障模式之间的交互中。你必须把两者都建模。

权衡：状态空间爆炸与抽象

模型检验不是免费的。状态数量随进程数与消息负载大小呈指数增长。一个包含五个值和三个接受者的规约可能产生数百万个状态。加入第四个接受者，数量就跃升到数十亿。在你的笔记本上跑，内存会在完成之前耗尽。

解决方案是抽象。你不是对实际的 64 字节值建模，而是对两个值建模：V1 和 V2。如果协议对两个值表现正确，具体值就无关紧要。你不对一万条记录的日志建模，而是对深度为 2 的日志建模。如果安全性对深度 2 成立，那它对任意深度几乎总是成立。这被称为 small-model checking，是该领域的标准做法。

关键技能在于学会区分哪些细节重要、哪些不重要。消息内容对安全性通常不重要。消息顺序几乎总是重要。节点身份也许不重要，但每个角色中的节点数量重要。

如果状态空间仍然太大，你还有其他选择。可以使用对称性归约，把相同的节点视为可互换。可以限制搜索深度。或者换用符号模型检验器如 Apalache，它利用 SMT 求解器在不枚举所有状态的情况下对状态进行推理。

从规约到实现：保持同步

经过验证的规约如果与实现背离，就毫无价值。规约是蓝图，代码是建筑。两者之间没有自动桥梁，而缝隙正是缺陷重新潜入的地方。

务实的做法是把 TLA+ 规约当作一份恰好可执行的设计文档。在代码审阅时一并审阅它。当实现处理了一个边界情况时，问问自己规约是否也处理了。当你在现网发现缺陷时，检查规约本能否逮住它。如果不能，更新规约。

有些团队更进一步，利用 TLC 产生的反例生成测试用例。一份展示两条副本如何分叉的 TLC 追踪，可以变成集成测试场景。这是手工活，但它把形式化模型与测试套件连接了起来。

在 Sentry，我们用这种方法验证了一个分布式限流协议。规约逮住了一个活性问题：某个恢复中的节点在特定分区场景下可能被饿死。我们的集成测试从未触发过它，因为它们总是干净地修复分区。模型检验器不在乎干净。它尝试了混乱的情况，发现了缺陷，让我们避免了一场非常令人困惑的事故。

入门：你的第一次模型检验

如果你想尝试，从 TLA+ Toolbox 开始。这是一款免费的 IDE，用于编写和检验规约。跟着它自带的 Paxos 和 Raft 示例练习。它们比上面的共识片段更复杂，但展示了真实协议如何被建模。

对于你的第一份规约，从自己的系统中挑一个小东西。一个领导者选举协议。一个分布式缓存失效方案。一个两阶段提交的变体。写下你相信成立的不变式。然后让 TLC 告诉你是否成立。答案通常是否定的，而且通常在一小时内就会告诉你。

模型检验不会找到所有缺陷。它对性能无能为力，抓不住序列化错误，也无法验证实现是否与规约一致。它的作用是找到集成测试漏掉的深层协议缺陷，而且在设计阶段就找到，此时修复成本为零。

这才是分布式系统中最廉价的缺陷修复。不是更好的调试器，不是更多的监控。而是在代码尚未存在之前就抓住缺陷。