Verisoft — 把整台计算机从门电路到邮件客户端全部用数学证完
待复核Verisoft 是 2003–2007 年德国国家出钱、Saarland 大学领头的一项工程：把一整台真能用的计算机——从最底层的门电路（逻辑门连成的芯片图纸，不是晶体管物理）、到处理器、到编译器、到操作系统、到上面跑的邮件客户端——每一层都用数学证明它是对的，并把证明拼成端到端定理。
日常类比：盖一栋楼。普通做法是各包工队各自验收，楼塌了互相推。Verisoft 是同一队人从打地基到装窗帘全程证明每一道工序对得上，最后给你一张总图：从泥土到楼顶每一层都有数学保证。
主导者是 Wolfgang Paul（Saarland）；合作方包括 DFKI、TU Munich、Infineon、BMW。Alkassar / Hillebrand / Leinenbach / Paul 把方法学总结成这篇 VSTTE 2008 报告。
如果不知道 Verisoft，下面这些事你会觉得很神奇但讲不清原理。
- 为什么 seL4（被数学证明正确的微内核）能成立——它与 Verisoft 同期并行（L4.verified），同属内核/全栈形式化谱系，方法学互相参照，并非 Verisoft 的直系产品线
- 为什么 CompCert（被证明正确的 C 编译器）能成立——和 Verisoft 同期同领域
- 为什么 Microsoft Hyper-V 在 2010 年前后做了大规模形式化验证——由后续项目 Verisoft XT 团队执行
- 为什么”软件全证明”在工业界仍罕见——主项四年（2003–2007）+ XT 延续、几十人、几十万行 Isabelle，成本极高
它标出了天花板：理论上能不能证明一整台机器？能。代价是什么？这么多。
方法叫 pervasive verification（穿透式验证）。三句话：
- 每一层都有数学规约（像盖楼先画图纸）：CPU 有 ISA 规约（指令集说明书：每条指令该做什么）、编译器有 C0→机器码对应、内核有系统调用规约、应用有行为规约。
- 每一层都证明实现 = 规约（像对照图纸验收施工）：门电路 = ISA、编译器 = 语义保持、内核 = 系统调用规约；主要在 Isabelle/HOL 里用 Isar（可读证明语言，像写带步骤的数学作业）完成，少量早期硬件工作用过 PVS。
- 接合定理把层连起来（像把各层验收单订成一本总册）：编译器证明告诉你「C0 在抽象语义里做的事 = 机器码在 VAMP 上做的事」；CPU 证明告诉你「VAMP 真在做 ISA 说的事」。两个一拼，得到「C0 程序 → 真硬件」端到端定理。这个「拼」才是 Verisoft 的核心贡献。
传统软件验证常在编译器或 OS 停住、假设硬件正确；Verisoft 不假设，一直证到门电路。
案例 1：VAMP 处理器——从门电路证起
Section titled “案例 1：VAMP 处理器——从门电路证起”VAMP 是一颗 DLX 风格的教学型 RISC（教科书里简化版 MIPS）。两层：
- 门电路层：寄存器、ALU、流水线用布尔逻辑写出
- ISA 层：抽象指令集，如「执行 ADD 做加法」
示意定理（教学伪代码，非可检 Isabelle）：
∀ n. gate_run(n_cycles) ≈ isa_run(k_instructions) -- k ≤ n（有 stall）逐部分解释：
gate_run：门电路按时钟一步步跑isa_run：按指令集说明书执行k ≤ n：流水线空转（stall）时，时钟比指令多
证完后可把硬件当 ISA 用。另有 Tomasulo 乱序版（指令可「插队」执行，像多窗口厨房同时炒多道菜）——并发证明更难。
案例 2：C0 编译器——为什么不是完整 C
Section titled “案例 2：C0 编译器——为什么不是完整 C”C0 是裁剪后的 C：无指针算术 / union / longjmp；整数溢出语义严格定义。完整 C 的未定义行为太多，证明完不成；C0 已够写邮件客户端与内核调度器。
∀ P. trace(compile(P) on VAMP) = trace(P in C0-semantics)逐部分解释：
- 任意合法 C0 程序 P
compile(P)得到机器码 P’- P’ 在 VAMP 上的执行轨迹，与 P 在 C0 抽象语义里的轨迹，在「内存映射」下一一对应
证完后不必再担心「编译器搞错」。
案例 3：CVM/VAMOS + 端到端
Section titled “案例 3：CVM/VAMOS + 端到端”CVM（Communicating Virtual Machines）是微内核抽象层——像「虚拟机之间怎么打电话」的说明书；VAMOS 建在其上（任务、IPC、驱动）。证明：内核代码 = 系统调用规约。
再叠应用层（C0 邮件客户端）+ 接合定理，总效果是：
合法 C0 程序 P 编成机器码放进 VAMP，跑 N 个时钟后，硬件状态对应 C0 语义里某一步——对应关系由编译器证明的内存映射给出。
中间任一层有 bug（流水线、寄存器分配、中断处理），总定理立刻破。能写出这句话还能机检通过，就是 Verisoft 的成绩。
- 接口规约比证明本身更难：层间约定（CPU 给编译器看什么状态？编译器给内核什么内存模型？）写错，下面证再多都白搭。
- C0 ≠ C：不能拿真 Linux 去证，必须用 C0 重写——证完的内核不是工业内核。
- 证明 ≠ 安全：只证「实现满足规约」；规约本身允许泄密，证完照样不安全。
- 代价与变更：几十万行证明；改一行实现可能重写几千行证明；完工后多数工件停止维护。
- 跟现实硬件有距离：VAMP 是教学 RISC，与 x86/ARM 无直接关系；XT 证 Hyper-V 时改以 x86 ISA 模型为底，不再下到门电路。
适用 vs 不适用场景
Section titled “适用 vs 不适用场景”适用：
- 高保证系统研究（航天、核控、密码硬件）——可接受「人年级」证明成本
- 教学：给学生看一遍「计算机栈全证明」长什么样
- 启发后续：seL4、CompCert、CakeML 的方法学参照
不适用：
- 普通工业软件——成本/收益不划算（数十人年量级）
- 快速演化系统——证明跟不上变更；且仅限 C0 + 教学 RISC，不覆盖完整 C / x86
- 「证完就安全」——证明只解决规约符合性的一半问题
历史小故事（可跳过）
Section titled “历史小故事（可跳过）”- 2003：BMBF 批准 Verisoft 主项，Wolfgang Paul 主持
- 2003–2007：四年主项，VAMP / C0 / CVM / VAMOS / 邮件客户端逐层推进
- 2007：Verisoft XT 启动，转向 Hyper-V、PikeOS 等工业系统
- 2008：本文在 VSTTE 发表，总结方法学与工件
- 2010 年后：项目收束；方法学被 NICTA seL4、MSR、INRIA CompCert 等继承；2014 年 CakeML 把自举式全栈证明推到 ML 编译器
- 2008 年前已证明「整机全栈证明」工程上可行——不是科幻
- 方法学比成品重要——穿透式验证、接合定理、Isar / locale 是留下的工具
- 真正瓶颈是规约——人想清楚「该保证什么」比工具查证明更难
- 工业界不照搬全栈，而做局部全证明——seL4 / CompCert / CakeML；接口契约写清，层与层才粘得住
- 证明工程需要工具链与回归——否则项目结束就归档，工件无法维护
- 论文 PDF：Alkassar et al. 2008 — The Verisoft Approach to Systems Verification（30 页综述）
- 项目归档：Verisoft Project Archive（论文、技术报告、Isabelle 源码）
- sel4 —— 同期内核验证高峰，工业可用微内核
- compcert —— 同期 C 编译器证明
- cakeml —— 自举式全栈证明 ML 编译器
- vamp-verisoft-2006 —— 栈底处理器证明细节
- isabelle-hol-2002 —— 主要证明工具，本项目推到规模极限
- hoare-logic —— 编译器与内核证明的基础逻辑
- sel4 —— 同期参照，专注高性能微内核
- compcert —— 同期 C 编译器证明
- cakeml —— 思路承接者，做到自举
- fstar —— 后代设计，规约+证明+实现合一
- vamp-verisoft-2006 —— Verisoft 栈底的处理器证明
- ironfleet-2015 —— IronFleet — 把分布式协议证到一行 bug 都没有
- vamp-verisoft-2006 —— VAMP — 把一颗有流水线、乱序、浮点和 cache 的处理器从门电路证到指令集