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

论文完整目标是 linearizability（线性一致性）：客户端看到的 put/get 顺序，像在一台机器上串行执行。教学上可先盯一条更直观的 SMR 安全性：

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

协议骨架长这样（伪代码）：

handleMessage(node, msg):
  match msg with
  | RequestVote ...   -> 更新 term / 投票
  | AppendEntries ... -> 追加日志、推进 commit
  return (新状态, 要发出的消息列表)

逐部分解释：handleMessage 是纯函数——给定当前节点状态和一条消息，算出新状态和出站消息；网络语义再决定这些消息会不会丢、重、乱序。证明流程：在较理想的语义下写不变量 → 用 Coq 战术证每条转移保持不变量 → 再经转换器搬到崩溃/丢包语义。完整 Raft 证明约 5 万行 Coq（实现本身只有几百行）。

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

假设你证了「语义 A 下，协议 P 满足性质 Q」。崩溃恢复类转换器大致做：

transformer(P) =
  P' where
    发送前：把关键状态写盘
    重启后：从盘恢复再继续
  + 证明：若 P ⊨ Q，则 P' ⊨ Q'（Q 的对应版本）

给协议加上持久化/恢复逻辑
给证明补上「崩溃事件不破坏 Q」的引理
输出新协议 P’ 及其证明

你写一遍应用逻辑，故障容忍由转换器搬运——这是 Verdi 最被引用的设计点。

案例 3：从 Coq 到能跑的 OCaml

Coq 的 extraction 把证过的函数翻成 OCaml。Verdi 把 Raft 提出来，再加一层网络 shim，做成键值存储 vard。PLDI 2015 评测里，vard 与同用 Raft 的 etcd 在吞吐/延迟上大致可比；正确性有机器检查，但生产仍常另写高性能实现（shim、数据结构、批处理都会差一截）。

踩过的坑

Coq 证明工程量巨大：完整 Raft 约 5 万行证明 ≈ 一篇博士论文；普通团队写不动，Verdi 侧多人写了约两年。
「故障转换器」覆盖不全：能搞定丢包、重复、崩溃恢复，但拜占庭故障（节点说谎）转不了；PBFT 一类协议 Verdi 帮不上。
「可执行」不等于「开箱即用生产」：extraction + shim 能跑，论文对 etcd 也报了可比数字；但缺批处理/更优数据结构时，生产仍常另写实现，不能把 vard 当现成 KV 产品。
证明依赖显式假设：网络与故障模型写在 Coq 里——模型错了证明也白搭。价值是让假设可见，不是让 bug 消失。
跨协议复用难：Raft 不变量库不能直接搬给 Paxos；Disel（2018）后来部分解决组合问题。
证明会随协议演化而腐化：Raft 后来有 corner case 修订，Verdi 证明不会自动跟，得手工改 Coq 再重证。

适用 vs 不适用场景

适用：

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

不适用：

只想找 bug 不要证明 → 用 TLA+ / P 这类模型检查器，几小时能跑
协议涉及拜占庭故障 → Verdi 转换器不支持
团队没 Coq 经验 → 学习成本以年计
要现成高性能 KV 产品 → 论文 demo 可比 etcd，但功能/工程完整度仍差一截
协议在快速迭代 → 改一行可能要重证很久

历史小故事（可跳过）

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 公理
可执行 ≠ 开箱即用——extraction 能跑通端到端，但生产路径常要另写实现补齐工程差距
工程量是真敌人——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 揉到一门语言里，分布式验证的另一条路

反向链接

disel-2018 —— Disel — 把分布式协议拆成可独立证明、可拼装的 Coq 模块