Verdi — 在 Coq 里完整证明 Raft 协议的分布式系统验证框架

是什么

Verdi 是华盛顿大学 2015 年做的一个让你在 Coq 里证明分布式协议正确的框架。日常类比：像写一部法律。你先在「文明社会」里把规矩立好（人人守约、信件不丢），再用一个叫网络转换器的工具，把规矩自动翻译到「乱世」（有人跑路、信件丢失、机器突然断电）。你只需要证明文明社会的版本，乱世版本由转换器代你搬运。

Verdi 团队最有名的成果：用 5 万行 Coq 证明了 Raft 共识协议——选主、日志复制、安全性全部机器检查通过，不是「一个人在论文里说对」，而是计算机一行行验证过没漏洞。

为什么重要

不理解 Verdi，下面这些事都没法解释：

为什么 2015 年之前的分布式协议论文里写的”已证明”基本不可信——Paxos 早期版本几年后才被发现 bug，Chord 论文里的算法被证伪
为什么金融、航空、共识协议这些「错一次死一次」的场景，工程界开始接受「写一年 Coq 比 debug 一年省」
为什么后续 IronFleet（2015，微软）/ Disel（2018）/ Chapar 都把 Verdi 当起点
为什么「形式化验证」不是数学家自娱——Verdi 提取的 OCaml 代码真能跑起来当 KV 存储

核心要点

Verdi 的设计可以拆成三层：

协议层：你在 Coq 里写协议——状态机、消息处理函数、初始状态。这一层和写普通函数式代码没差别。
网络语义层：定义「网络允许做什么坏事」的数学规则。Verdi 提供一系列预设语义：
- 理想网络（不丢不重不乱序，没崩溃）—— 最容易证
- 丢包网络（消息可能丢）
- 重复网络（消息可能送两次）
- 崩溃恢复网络（节点可能突然挂掉再起来）
网络转换器：核心创新。它是一个Coq 函子（functor）——输入「理想网络下证好的系统」，输出「故障网络下也证好的系统」。证明跟着自动搬过去，你不用重写。

三层加起来叫 Verdi 工作流：先在天堂里证，再让转换器把证明搬到地狱。

实践案例

案例 1：Verdi 怎么证 Raft

Raft 在 Verdi 里被证的目标叫 State Machine Replication（SMR）安全性：

任何两个节点已提交（committed）的日志位置 i，存的命令必须相同。

证明流程：

在「理想网络」里写 Raft：选主、AppendEntries、心跳——大约 1 万行 Coq
在 Coq 里写不变量（invariant）：「任何时刻，已提交的日志前缀在所有正常节点上一致」
用 Coq 战术（tactics）一步步证明每条状态转移都保持不变量——大约 4 万行
调用 Verdi 的「崩溃恢复转换器」，自动得到「真实网络下 Raft 也满足 SMR」

整个工程：3 个博士生、2 年时间、约 50000 行 Coq。

案例 2：网络转换器到底干了什么

假设你证了「理想网络下，协议 P 满足性质 Q」。崩溃恢复转换器会：

自动给协议 P 加上「持久化日志」逻辑——崩溃前的状态写盘，重启后恢复
自动给证明加上「崩溃事件不破坏 Q」的引理
输出新的协议 P_crash 和它满足 Q 的证明

你写了一遍，得到两个版本。这是 Verdi 论文里最被引用的设计点。

案例 3：从 Coq 到能跑的 OCaml

Coq 有个叫 extraction 的功能：把证好的 Coq 函数翻译成 OCaml 代码。Verdi 团队用它把 Raft 提取成 OCaml，再加一层网络栈，做成了一个能真跑的键值存储——叫 vard。

vard 的客户端可以连，可以 put/get，节点崩溃后能恢复。性能比手写 Raft 慢约 10 倍，但正确性是数学证过的。

案例 4：转换器为什么是「函子」

如果你把一份协议看成「数据 + 操作」，把网络看成「环境」，那么 Verdi 的转换器就是数学上的函子——一个把「环境 A 上的协议」映射成「环境 B 上的协议」的高阶构造，且保持结构（你证好的不变量自动跟着搬）。

这一步在 Coq 里写成大约 800 行的通用证明骨架，所有协议都共享。新协议接入时不必重写转换器，只需把协议本身证好，转换器替你把丢包/崩溃这些坏事的证明部分补上。

踩过的坑

Coq 证明工程量巨大：Raft 5 万行 Coq ≈ 一篇博士论文工作量。普通团队写不动；Verdi 团队三人写两年。
「故障转换器」覆盖不全：转换器能搞定丢包、重复、崩溃恢复，但拜占庭故障（节点说谎）转不了。涉及恶意节点的协议（PBFT 等）Verdi 帮不上。
「可执行」不等于「性能好」：Coq 提取出的 OCaml 代码用了大量函数式构造（无副作用、闭包包闭包），比手写 C/Rust 慢一个数量级。vard 不能直接当生产 KV 用。
证明依赖一堆假设：时钟同步、调度公平性、消息延迟上界——这些假设在 Coq 里被显式列出，假设错了证明也白搭。Verdi 的价值是让假设可见，不是让 bug 消失。
跨协议复用难：Verdi 证 Raft 的不变量库不能直接搬给 Paxos 用。Disel（2018）后来部分解决了这个问题。
证明会随协议演化而腐化：Raft 论文后来出了几个 corner case 修订（如 leader 切换时的日志覆盖规则），Verdi 的证明不会自动跟，得手工把改动反映到 Coq 里再重证一遍。

适用 vs 不适用场景

适用：

关键系统（金融清算、航空控制、区块链共识）愿意为正确性投半年到两年
团队有 Coq / Isabelle / Lean 经验，且至少 1 个高手镇场
协议规模可控（Raft / 2PC / 简单 Paxos），不是整个微服务全家桶
重视「假设显式化」——把所有隐含假设上墙，用证明逼出来

不适用：

只想找 bug 不要证明 → 用 TLA+ / P 这类模型检查器，几小时能跑
协议涉及拜占庭故障 → Verdi 转换器不支持
团队没 Coq 经验 → 学习成本两年起步
性能敏感场景 → Verdi 提取代码比手写慢 10 倍
协议在快速迭代 → 改一行可能要重证一周

历史小故事（可跳过）

1990s—2000s：分布式协议靠人脑论文证明。Paxos 早期版本几年后才被发现 corner case bug，Chord 论文里的算法被反例证伪。
1994—2002：Lamport 推 TLA+，让工程师用模型检查找反例。能找 bug，但找不到「没 bug」的数学保证。
2010：Raft（Ongaro & Ousterhout）让共识协议可读懂，给形式化打开了门——之前的 Paxos 论文太抽象，没法直接搬到 Coq。
2015 PLDI：Wilcox 等人发表 Verdi，同年微软 IronFleet 用 Dafny + TLA 走了另一条路。两条路线之争至今没分胜负。
2018：Disel（Sergey 等）把 Verdi 思路精简，引入「组合证明」——一个协议的证明可以拼到另一个里。

之后 10 年，分布式系统形式化验证从「学术玩具」变成「特定场景的工业选项」。

学到什么

「理想模型 + 故障转换器」是可推广的套路——先在简单世界证明，再加干扰一层一层套，每层只证「干扰不破坏性质」
形式化验证不是「让 bug 消失」，是让假设显式化——所有隐含假设被逼到台面上写成 Coq 公理
可执行 ≠ 性能好——Coq 提取代码慢得令人发指，形式化验证目前只在「正确性 >> 性能」的场景里赢
工程量是真敌人——5 万行 Coq 证明的回报，需要十年使用周期才能赚回来。短命系统不值得证
学界 vs 工业——Verdi 是学界范例，工业界更接受 TLA+（找反例性价比高）。理解两条路的取舍才能选对工具

关联

raft —— Verdi 证的核心协议；理解 Raft 才能看懂 Verdi 在证什么
ironfleet-2015 —— 同年微软用 Dafny + TLA 做的对手方案，路线对比
paxos-1998 —— 共识协议鼻祖；Verdi 也证过简单 Paxos
lamport-tla-1994 —— TLA 走模型检查路线，Verdi 走定理证明路线，两条路互补
tla-yu-tlc-1999 —— TLC 是 TLA 的模型检查器，找反例的代表
calculus-of-constructions —— Coq 的理论基础；Verdi 的依赖类型来自这里
stainless-2017 —— 给 Scala 函数做类似的证明工作，工程量友好得多
fstar —— 把依赖类型 + SMT 揉到一门语言里，分布式验证的另一条路

反向链接

calculus-of-constructions —— Calculus of Constructions — 让程序和数学证明共用一种语言
disel-2018 —— Disel — 把分布式协议拆成可独立证明、可拼装的 Coq 模块
fstar —— F* — 把依赖类型、SMT 自动化、副作用追踪揉到一门语言里
lamport-tla-1994 —— TLA — 把状态机和时序逻辑捏成一个公式
paxos-1998 —— Paxos 1998 — 古希腊议会寓言里藏的共识协议
raft —— Raft — 易理解的共识算法
stainless-2017 —— Stainless — 让编译器替你证明 Scala 函数真的满足规约
tla-yu-tlc-1999 —— TLC — 让 TLA+ 规范可以一键机检的模型检查器