Verisoft — 把整台计算机从晶体管到邮件客户端全部用数学证完

是什么

Verisoft 是 2003-2007 年德国国家出钱、Saarland 大学领头的一个疯狂的工程：把一整台真能用的计算机——从最底层的晶体管电路、到处理器、到编译器、到操作系统、到上面跑的邮件客户端——每一层都用数学证明它是对的，而且把所有证明拼起来，得到一个端到端定理。

日常类比：盖一栋楼。普通做法是建筑公司证地基没问题、钢筋公司证钢筋没问题，最后楼塌了大家互相推。Verisoft 的做法是同一队人从打地基到装窗帘全程证明每一道工序对得上，最后给你一张总图：从泥土到楼顶每一颗螺丝都有数学保证。

主导这件事的是 Wolfgang Paul（Saarland 大学），合作方包括 DFKI、TU Munich、Infineon、BMW。论文里署名的 Alkassar / Hillebrand / Leinenbach / Paul 是把整个项目方法学总结成一篇 VSTTE 2008 报告的人。

为什么重要

如果不知道 Verisoft，下面这些事你会觉得很神奇但讲不清原理。

• 为什么 seL4（号称”世界上唯一被数学证明正确的微内核”）能成立——它是 Verisoft 思路的直系后代
• 为什么 CompCert（被数学证明正确的 C 编译器）能成立——和 Verisoft 同期同领域
• 为什么 Microsoft 的 Hyper-V hypervisor 在 2010 年前后做了大规模形式化验证——直接由 Verisoft XT 团队执行
• 为什么”软件全证明”在工业界仍然罕见——Verisoft 已经告诉你答案：10 年、几十人、几十万行 Isabelle 证明，太贵

它定义了一个领域的天花板：理论上能不能证明一整台机器？能。代价是什么？这么多。

核心要点

Verisoft 的方法叫 pervasive verification（全栈/穿透式验证）。核心思想三句话讲完。

1. 每一层都有数学规约：CPU 有规约（指令集语义）、编译器有规约（C0 源代码语义到机器码语义的对应）、内核有规约（系统调用做了什么）、应用有规约（邮件客户端的行为）。

2. 每一层都证明实现 = 规约：CPU 的电路图 = ISA 规约（在 Isabelle 里证）、编译器的代码 = C0→机器码语义保持（在 Isabelle 里证）、内核的代码 = 系统调用规约（在 Isabelle 里证）。

3. 接合定理把层与层连起来：编译器证明告诉你”C0 程序在抽象语义里做的事，编译后机器码在 VAMP 上做同样的事”。CPU 证明告诉你”VAMP 真在做 ISA 规约里说的事”。两个一拼，你就有了”C0 程序 → 真硬件” 的端到端定理。这个”拼”才是 Verisoft 真正的贡献。

证明工具用的是 Isabelle/HOL（少量 PVS），证明语言用的是 Isar。

为什么这三步够用？因为它们对应着工程师写代码的三件事：定义”我想做什么”（规约）、写”我怎么做”（实现）、确认”这两个对得上”（证明）。Verisoft 的特别之处是把这套流程严肃到 CPU 门电路这一层——传统软件验证在编译器或 OS 就停了，下面假设硬件正确。Verisoft 不假设。

实践案例

案例 1：VAMP 处理器——从门电路证起

VAMP 是一颗 DLX 风格的 RISC 处理器（教科书上常用的简化 MIPS）。它在 Isabelle 里被表达为两层。

• 门电路层：每个寄存器、ALU、流水线段都用布尔逻辑写出来
• ISA 层：抽象指令集，“执行 ADD 指令做加法”

证明定理：门电路层运行 N 个时钟周期 = ISA 层执行 K 条指令（K ≤ N，因为有流水线 stall）。这个定理几千页 Isabelle，证完之后你就可以把硬件当 ISA 用，不再担心晶体管。

VAMP 还做了 Tomasulo 乱序执行版本——并发证明，更难。

案例 2：C0 编译器——为什么不是完整 C

C0 是裁剪后的 C 子集：

• 没有指针算术（p++、p[i] 形式只允许数组）
• 没有 union
• 没有 longjmp、不定参数函数
• 整数溢出语义被严格定义

裁剪是工程妥协：完整 C 的”未定义行为”太多，证明不可能完成。C0 已经够写邮件客户端、内核任务调度器了。

编译器证明的核心定理：对任何 C0 程序 P，编译产物 P-prime 在 VAMP 上的执行轨迹 = P 在 C0 抽象语义里的执行轨迹。这个定理一旦证完，你就再也不用担心”编译器搞错”。

案例 3：CVM/VAMOS 内核——OS 也能证

CVM = Communicating Virtual Machines，是一个微内核抽象层。VAMOS 是建在 CVM 之上的真微内核（任务、IPC、设备驱动）。证明：内核代码 = 系统调用规约。

到这一步，你已经有了：硬件 ✓ 编译器 ✓ 内核 ✓。再写邮件客户端用 C0 写、用 VAMOS 系统调用，应用层证明 + 接合 = 端到端。这就是 Verisoft 真正交付的东西。

案例 4：端到端定理长什么样

最后那个”拼起来”的总定理，用日常话说大致是：

对任何用 C0 写的合法程序 P，把 P 编成机器码 P-prime 放进 VAMP 真硬件里，让它跑 N 个时钟周期：硬件最终的状态对应着 C0 抽象语义里 P 跑到某一步时的状态——这个对应关系由编译器证明里的”内存映射”给出。

中间任何一层有 bug（CPU 流水线、编译器寄存器分配、内核中断处理），这个总定理都立刻会破。能写出这句话还能机检通过，就是 Verisoft 真正的成绩。

踩过的坑

1. 接口规约比证明本身更难：每一层之间的”约定”（CPU 给编译器看到什么状态？编译器给内核看到什么内存模型？）写错了，下面证再多都白搭。Verisoft 团队花了大量精力定义和修正这些接口。

2. C0 不等于 C：你不能拿一个真 Linux 内核去证明，必须用 C0 重写。这是项目最大的实用性争议——证完的内核不是工业内核。

3. 证明 ≠ 安全：证明的是”实现满足规约”。如果你的规约本身允许 root 给所有人看密码，证完了系统照样不安全。Verisoft 不解决”该规约什么”。

4. 代价巨大：累计几十万行 Isabelle 证明、几十名博士、10 年。完工时项目结束，多数证明工件没有继续维护。

5. 变更难传播：改一行 C0 编译器实现，关联的证明可能要重写几千行。不像普通工程”测试再跑一遍”，证明工程里改动是真痛。

6. 跟现实硬件有距离：VAMP 是教学型 RISC，不是 x86 也不是 ARM。证完之后跟英特尔 CPU 没有直接关系。Verisoft XT 后来去证 Hyper-V 时不再下到 CPU 层，改用 x86 ISA 模型作为底。

适用 vs 不适用场景

适用：

• 安全/安保关键系统的研究——核电站控制、航天、密码硬件
• 教学和学术——给学生看一遍”计算机栈全证明长什么样”
• 启发后续项目——seL4、CompCert、CakeML 都从这里学方法论

不适用：

• 普通工业软件——成本/收益比完全不划算
• 快速演化的系统——证明跟不上代码变更速度
• “证完就安全了”的诉求——证明只解决一半的问题

历史小故事（可跳过）

• 2003 年：BMBF（德国教育与研究部）批准 Verisoft 主项，Wolfgang Paul 拿下大笔经费
• 2003-2007 年：四年苦战，VAMP/C0/CVM/VAMOS/邮件客户端逐层证完
• 2007 年：Verisoft XT 启动，转向工业系统：Microsoft Hyper-V、SYSGO PikeOS
• 2008 年：本论文在 VSTTE 发表，把方法学和工件总结给学界
• 2010 年后：项目自然结束，Wolfgang Paul 退休，方法学被 NICTA seL4、Microsoft Research、INRIA CompCert 团队继承
• 2014 年：CakeML 出现，把”自举式全栈证明”思路推到 ML 编译器

学到什么

1. 完整证明一台机器在 2008 年已经被证明可行——不是科幻，是工程
2. 方法学比成品重要——pervasive verification、接合定理、Isar 证明语言、Isabelle locale，都是这一波研究留下的”工具”
3. 证明的真正瓶颈是规约——写规约（人来想）比证明（工具帮你查）难得多
4. 工业界为什么不照搬——成本太大；但 sel4 / CompCert / CakeML 这些”局部全证明”项目继承了 Verisoft 精神
5. 接口规约是层与层粘合的胶水——这一点放到任何工程领域都成立：契约写清楚，下面好做；契约模糊，下面再用力都白费
6. 证明工程不是科研项目而是工业品——需要工具链、CI、回归测试，否则项目结束就归档

延伸阅读

• 论文 PDF：Alkassar et al. 2008 — The Verisoft Approach to Systems Verification（30 页综述，密度大但不要求读懂证明细节）
• 项目主页归档：Verisoft Project Archive（论文、技术报告、Isabelle 源码下载）
• sel4 —— 受 Verisoft 启发、只证内核但完工的工业级项目
• compcert —— 同期同行，证 C 编译器
• cakeml —— 自举式全栈证明 ML 编译器，思路承接 Verisoft

关联

• isabelle-hol-2002 —— Verisoft 的主要证明工具，本项目把它推到了规模极限
• hoare-logic —— 编译器和内核证明的基础逻辑
• sel4 —— 直系后代，专注内核
• compcert —— 同期 C 编译器证明，方法学互相借鉴
• cakeml —— 思路承接者，做到了自举
• fstar —— 后代设计，把规约+证明+实现合并到一种语言

一句话总结

Verisoft = 用 10 年时间和几十名博士，亲手证明了”从晶体管到邮件客户端整条链都能用数学保证”。代价昂贵到不可复制，但留下了 sel4、CompCert、CakeML 等一系列直接受益的”局部全证明”工业品。

反向链接

• cakeml —— CakeML — 从源码到机器码每一步都被数学证明的 ML 编译器
• compcert —— CompCert — 每条优化都被数学证明保持语义的 C 编译器
• fstar —— F* — 把依赖类型、SMT 自动化、副作用追踪揉到一门语言里
• hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
• ironfleet-2015 —— IronFleet — 把分布式协议证到一行 bug 都没有
• vamp-verisoft-2006 —— VAMP — 把一颗有流水线、乱序、浮点和 cache 的处理器从门电路证到指令集