Why3 — 写一次程序规范，多个证明器一起来证

是什么

Why3 是一个程序验证平台：你用它的语言 WhyML 写代码 + 写”代码应该满足什么”，平台自动把这些条件翻译成数学题，同时丢给好几个证明器（Z3、Alt-Ergo、CVC4、Coq…）去解。

日常类比：像考试时把同一道难题复印多份发给一屋子专家——有人擅长代数、有人擅长几何。谁先解出来，你就接受谁的答案；都解不出，再自己人工补刀。

你写：

let factorial (n: int) : int
  requires { n >= 0 }
  ensures  { result >= 1 }
= ...

requires / ensures 就是你给函数的”出题”。Why3 自动生成”如果 n >= 0，那么 result >= 1”这道证明题，然后分发出去。

为什么重要

不理解 Why3，下面这些事都不好理解：

• 为什么 SPARK / Frama-C / CryptoLine 这些验证 C / Ada 代码的工具，背后跑的都是同一个引擎
• 为什么”证明器多样化”是工程必需——同一道题 Z3 卡 30 秒、Alt-Ergo 0.1 秒，反过来也常见
• 为什么 F*、Dafny、Viper 这些后辈的设计都绕不开”VC 生成 + 多后端”这条路
• 为什么 2013 年的工具到 2026 年还在更新——它解的是”中间表示”问题，跟具体证明器解耦

核心要点

Why3 的设计可拆成 三层：

1. 前端（WhyML）：带契约的 ML 风格语言。支持纯函数、异常、可变引用、循环不变量。还可以写 ghost code——只为了证明而存在，编译生成可执行代码时会被擦掉。

2. 中间层（VC 生成器）：基于 Hoare 逻辑里的 weakest precondition 演算（hoare-logic）。把”程序 + 契约”翻译成一堆纯逻辑公式，叫 verification conditions（VC）。

3. 后端（driver）：每个证明器（Z3 / Alt-Ergo / CVC4 / Coq / Isabelle）配一个驱动文件，声明：这个证明器支持哪些理论、关键字怎么翻译、不支持的算子怎么编码。同一组 VC 可以同时打给 N 个后端。

平台不发明新理论，它发明的是”解耦”——程序员、证明义务、证明器三者各干各的。

类比：Why3 之于程序验证，相当于 LLVM 之于编译——前者把”程序+规范”折成一种通用 IR 喂给一群求解器，后者把源语言折成 LLVM IR 喂给一群目标后端。两边都是靠中间表示分摊生态。

实践案例

案例 1：写一道带循环不变量的题

let sum_to (n: int) : int
  requires { n >= 0 }
  ensures  { result = n * (n + 1) / 2 }
= let ref s = 0 in
  for i = 1 to n do
    invariant { s = i * (i - 1) / 2 }
    s <- s + i
  done;
  s

Why3 看到 for 循环，强制你写 invariant（循环每轮都成立的事实）。它把”进入循环时不变量成立”、“循环体保持不变量”、“退出后由不变量推出 ensures”三道子题都生成出来分发。

案例 2：自动器卡住，人工 Coq 接力

某些 VC 涉及复杂归纳（比如关于树高度的不等式），SMT 求解器（z3-2008 等）会超时。Why3 IDE 里你可以右键这道题”切到 Coq”，平台直接生成对应的 Coq 证明脚手架，你只在 Coq 里手写归纳那一步，其他部分还是自动。

这种”自动 90% + 人工 10%“是 Why3 工程上能落地的关键。

案例 3：CryptoLine 借 Why3 证密码代码

CryptoLine 把 C 写的椭圆曲线乘法、AES 这类位级密码代码翻译到 WhyML，再用 Why3 的多后端验证 “这段代码计算的 modular 结果跟数学定义一致”。Z3 处理位向量约束、Coq 处理代数性质——分工明确。

案例 4：ghost code 帮证不影响运行

let pop (q: queue 'a) : 'a
  requires { not (is_empty q) }
= ghost let old_size = size q in
  let x = ... in
  assert { size q = old_size - 1 };
  x

ghost 关键字标记的变量只在证明阶段存在。编译成 OCaml 时被整段擦掉，运行时零开销。这让程序员可以放手在代码里加”证明用变量”，不用怕拖慢生产代码。

踩过的坑

1. VC 数量爆炸：一个看似简单的函数，因为分支多、循环多、契约多，可能生成几百道 VC。需要靠后端缓存 + 并行 + 选择性触发证明来扛。

2. WhyML 不是”通用语言”：它没设计成给人写产品代码用的。要验证 C / Ada / Rust，得先翻译进 WhyML，翻译器（Jessie、SPARK、Creusot）本身就是大工程。

3. 驱动文件写错全盘崩：把 mod 翻译成 Z3 的 bvurem 还是 mod，参数顺序错了，证明器返回 “unsat” 但其实题目本身被歪曲了。Why3 团队为此积累了上千行的标准 driver 库。

4. 自动器之间不互通：Z3 解出来 Alt-Ergo 不一定信。Why3 不复用证明结果，每个后端各跑各的——好处是简单，代价是浪费算力。

5. 别名（alias）很难处理：可变引用一旦指向同一块内存，VC 推导会爆炸。Why3 用类型不变量 + region 推断避免别名进入逻辑层；代价是 WhyML 写起来比通用 ML 多几条限制。

适用 vs 不适用场景

适用：

• 验证已有命令式代码（C / Ada / Rust）正确性 → 通过 Frama-C / SPARK / Creusot 接 Why3
• 密码库、操作系统内核、关键算法的功能正确性证明
• 想要”自动证明优先 + 人工证明兜底”的混合工作流

不适用：

• 验证机器学习模型（值域是浮点 + 概率，不是离散逻辑）
• 验证 UI / 网络协议交互（属于时序验证，更适合 lamport-tla-1994）
• 写日常应用代码——成本远高于收益

历史小故事（可跳过）

• 1990 年代：Filliâtre 在巴黎南大博士期间做 Why（v1），原型只接 Coq 后端
• 2003 年：Why2 加入多后端支持，Frama-C / Jessie 开始用
• 2010 年：Filliâtre + Paskevich 重写为 Why3，前端从 ML 子集改造成完整 WhyML
• 2013 年：ESOP 论文正式介绍 Why3 平台，成为欧洲程序验证的事实标准
• 同代竞品 Boogie（boogie-2005，Microsoft）走类似思路但更轻量；F*（fstar）则把 Why3 思路 + 依赖类型揉到一门语言里

学到什么

1. 解耦比创新更工程化：Why3 没发明新证明算法，它发明了”前端 / VC / 后端”的分层，让生态可以独立演化
2. 多后端不是冗余而是必需：不同求解器擅长不同理论，工程上赌单一后端会很疼
3. 自动 + 人工的边界要可移动：靠 driver + IDE 让程序员能在任意一道 VC 上”降级”到人工证明
4. 中间语言比通用语言重要：WhyML 自己不流行，但它作为翻译目标承载了 Frama-C / SPARK / CryptoLine 的全部底层

延伸阅读

• 论文 PDF：Why3: Where Programs Meet Provers (ESOP 2013)
• 官网：why3.lri.fr — 含教程、driver 文件、IDE
• 教程 gallery：Why3 Examples — 几百道带规范的练习题
• hoare-logic —— Why3 VC 生成的逻辑底座
• boogie-2005 —— 同代另一条多后端验证中间语言路线
• z3-2008 —— Why3 最常用的 SMT 后端
• fstar —— 现代继承者，把 Why3 思路 + 依赖类型合一

关联

• hoare-logic —— Why3 把 Hoare 三元组系统化成 VC 生成器
• boogie-2005 —— Microsoft 同代竞品；Boogie 偏轻量、Why3 偏完整
• z3-2008 —— SMT 求解器，Why3 默认后端之一
• isabelle-hol-2002 —— 当自动器卡住时的人工后端选项
• fstar —— Why3 思路的现代继承者

反向链接

• fstar —— F* — 把依赖类型、SMT 自动化、副作用追踪揉到一门语言里
• hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
• lamport-tla-1994 —— TLA — 把状态机和时序逻辑捏成一个公式
• vcc-2009 —— VCC — 给并发 C 加注解，让 SMT 自动证它对
• z3-2008 —— Z3 2008 — 把 SMT 工程化到工业默认