什么是形式化验证？

形式化验证是用数理逻辑证明一个程序或硬件设计对每一种可能的输入或行为都满足精确的规约。测试只检查部分情况，而一次完成的验证覆盖全部情况，前提是相对于所用的规约以及被验证的系统模型。

什么是 Hoare 逻辑？

Hoare 逻辑由 C. A. R. Hoare 于 1969 年提出，是一套建立在三元组 {P} S {Q} 之上的程序证明系统：如果命令 S 执行前前置条件 P 成立且 S 终止，则执行后后置条件 Q 成立。它的规则涵盖赋值、顺序、条件和循环；循环需要不变式。它是现代演绎式程序验证器的基础。

什么是模型检测？

模型检测是一种自动技术，它通过遍历状态来判定一个系统的有限状态模型是否满足一条时序逻辑性质。如果性质不成立，模型检测器会给出一条反例执行。它由 Clarke 与 Emerson 以及 Queille 与 Sifakis 在 20 世纪 80 年代初提出，三人因此获得 2007 年图灵奖。

LTL 和 CTL 有什么区别？

LTL 即线性时序逻辑，描述单条执行的性质，例如 G(req → F grant)：在每次运行中，每个请求终将被授予。CTL 即计算树逻辑，对分叉的未来做量化，例如 EF grant：从这里出发，存在某条执行能到达授予。两者各自能表达对方无法表达的性质；CTL* 同时包含两者。

什么是抽象解释？

抽象解释由 Patrick Cousot 与 Radhia Cousot 于 1977 年提出，是一套可靠静态分析的理论。它在抽象值（例如符号或区间）上运行程序，这些抽象值过近似了每一次真实执行。如果近似显示没有错误，程序就没有错误；否则分析器发出警报，而警报可能是误报。

什么是程序综合？

程序综合是根据规约自动构造程序。演绎式综合从“规约可以被满足”的构造性证明中抽取程序；归纳式综合，例如 Excel 的 Flash Fill，在受限语言中搜索与输入输出示例一致的程序；语法制导综合把逻辑规约与文法结合起来。

SMT 求解器在验证中有什么用？

验证器把程序及其规约变成称为验证条件的逻辑公式。Z3 等 SMT 求解器在整数、位向量、数组等理论上判定这些公式是否可满足。当一个条件的否定不可满足时，该条件就被证明有效；否则求解器通常会返回一个反例。

形式化验证是否意味着软件没有缺陷？

不是。它意味着软件在所述假设下满足其规约。缺陷仍可能存在于规约、未验证的组件、硬件或被信任的工具中。即便如此，对已验证的 CompCert 编译器进行随机测试，在其已验证部分中没有发现错误代码生成的问题，这正是人们愿意付出这份努力的原因。

符号 AI 技术 · 验证与综合

形式化验证与程序综合

证明一个程序做到了规约所说的事，以及首先从规约推导出程序。Hoare 逻辑、模型检测、项重写与 Knuth–Bendix 完备化、抽象解释、基于 SMT 的验证、演绎式与基于示例的综合，以及已验证系统 CompCert 与 seL4。每一项都附有算例，并如实说明其局限。

Perslis Research · 2026-09-26

形式化验证是用数理逻辑证明一个程序或系统对每一种可能的输入或行为都满足精确的规约，而不仅仅是测试碰巧尝试过的那些情况。程序综合是反方向的任务：根据规约、一组示例或两者，自动构造出程序。

一段话概述

测试只是对行为抽样；验证覆盖全部行为。1969 年，C. A. R. Hoare 在 Floyd 1967 年工作的基础上，给出了证明程序性质的规则，即 Hoare 三元组。20 世纪 80 年代初，Clarke 与 Emerson，以及独立工作的 Queille 与 Sifakis，证明有限状态系统可以针对时序逻辑性质被自动检查：这就是模型检测，性质不成立时它会给出一个反例。项重写赋予等式推理一种可计算的形式，Knuth 与 Bendix（1970）展示了如何把一组等式完备化为一个收敛的重写系统。抽象解释（Cousot 与 Cousot，1977）通过计算过近似，使静态分析变得可靠。如今，Z3 等 SMT 求解器自动解决了大部分逻辑附带条件。程序综合把这条流水线倒过来运行，从 Manna 与 Waldinger 的演绎方法，到 FlashFill 的示例编程。最有力的成果是完整的已验证系统：CompCert C 编译器与 seL4 微内核。局限在于：Rice 定理排除了对任意程序进行全自动、精确分析的可能，状态空间会爆炸，而每个证明都是相对于一个本身可能出错的规约而言的。

本页是符号 AI 技术下的一个家族页面。这里的方法用到了逻辑编程与定理证明中的逻辑与证明机制，以及约束满足、SAT 与 SMT 中的求解器。关于整个领域，见什么是符号 AI？与符号 AI 的历史。

1. 演绎式验证：Hoare 逻辑及其后继者

Hoare 逻辑

谁、何时。C. A. R. Hoare，《An Axiomatic Basis for Computer Programming》，Communications of the ACM，1969 年 [1]。它建立在 Robert Floyd 的《Assigning Meanings to Programs》（1967）之上，后者把断言附加到流程图上 [2]。这个系统常被称为 Floyd–Hoare 逻辑。

是什么。Hoare 三元组 ${P} S {Q}$ 的意思是：如果命令 $S$ 运行前前置条件 $P$ 成立，并且 $S$ 终止，那么之后后置条件 $Q$ 成立。这是部分正确性；完全正确性还要求证明终止。核心规则如下：

\begin{matrix} {P [E / x]} x := E {P} & \frac{{P} S {Q} {Q} T {R}}{{P} S; T {R}} \\ \frac{P \to P^{'} {P^{'}} S {Q^{'}} Q^{'} \to Q}{{P} S {Q}} & \frac{{I \land b} S {I}}{{I} while b do S {I \land \neg b}} \end{matrix}

从左上角顺时针读：赋值公理、顺序组合、推论规则，以及带循环不变式 $I$ 的 while 规则。

算例：赋值公理。在 $y := x + 1$ 之前必须有什么成立，才能使之后 $y > 10$ 成立？公理用反向代入来回答：在后置条件中把 $y$ 换成 $x + 1$ 。

{x + 1 > 10} y := x + 1 {y > 10} 且在整数上 x + 1 > 10 ⟺ x > 9

因此 ${x > 9} y := x + 1 {y > 10}$ ，而由推论规则，任何更强的前置条件，比如 $x = 42$ ，也都成立。关键在于反向：它把程序文本变成一条求解器可以检查的逻辑公式。

一个循环。对程序 i := 0; s := 0; while i < n do (i := i + 1; s := s + i)，前置条件为 $n \geq 0$ ，取不变式

I \equiv s = \frac{i (i + 1)}{2} \land i \leq n

初始化之后它成立（ $0 = 0$ ， $0 \leq n$ ）。若它成立且 $i < n$ ，执行一次迭代得到 $s^{'} = \frac{i (i + 1)}{2} + (i + 1) = \frac{(i + 1) (i + 2)}{2}$ 且 $i + 1 \leq n$ ，所以不变式得以保持。退出时 $I \land i \geq n$ 迫使 $i = n$ ，从而 $s = n (n + 1) / 2$ 。量 $n - i$ 不断减小且保持非负，这就证明了终止。

今天用在哪里。所有“自动主动式”验证器（Dafny、Why3、Frama-C 的 WP 插件、SPARK）都以这种方式生成验证条件。局限。必须有人找出循环不变式，而且上述规则不能很好地处理指针、别名或并发；下面两项正是针对这些问题的。

最弱前置条件

谁、何时。Edsger W. Dijkstra，《Guarded Commands, Nondeterminacy and Formal Derivation of Programs》，Communications of the ACM，1975 年 [3]。是什么。一种谓词变换器： $wp (S, Q)$ 是保证 $S$ 终止于满足 $Q$ 的状态的最弱条件。它按结构计算： $wp (x := E, Q) = Q [E / x]$ ， $wp (S; T, Q) = wp (S, wp (T, Q))$ 。当 $P \to wp (S, Q)$ 有效时，程序是正确的。Dijkstra 用这套演算从规约推导程序，这也使它成为程序综合的先驱之一。

分离逻辑

谁、何时。John C. Reynolds、Peter O’Hearn、Samin Ishtiaq 与 Hongseok Yang，1999–2002 年；Reynolds 在 LICS 2002 上的论文是标准参考文献 [4]。是什么。针对操作指针的程序对 Hoare 逻辑的扩展。分离合取 $P * Q$ 表示堆可以分成两个不相交的部分，分别满足 $P$ 和 $Q$ 。由此得到框架规则，它让关于一部分内存的证明可以忽略其余部分：

\frac{{P} C {Q}}{{P * R} C {Q * R}} （ C 不修改 R 中的任何自由变元）

今天用在哪里。Meta 的 Infer 于 2015 年开源，它把分离逻辑与双向溯因（bi-abduction）结合，在大型代码库中于上线前发现内存和资源错误 [5]。Stephen Brookes 与 Peter O’Hearn 因并发分离逻辑获得 2016 年哥德尔奖。

2. 模型检测与时序逻辑

时序逻辑：LTL 与 CTL

谁、何时。Amir Pnueli 的《The Temporal Logic of Programs》（FOCS 1977）把时序逻辑引入计算机科学，用来陈述持续运行的反应式程序的性质 [6]；他因此获得 1996 年图灵奖。线性时序逻辑（LTL）谈论单条无穷执行。在路径 $π = s_{0} s_{1} s_{2} \dots$ 上，记 $π^{i}$ 为从 $s_{i}$ 开始的后缀：

\begin{array}{l} π ⊨ X φ & ⟺ & π^{1} ⊨ φ \\ π ⊨ F φ & ⟺ & \exists i \geq 0 : π^{i} ⊨ φ \\ π ⊨ G φ & ⟺ & \forall i \geq 0 : π^{i} ⊨ φ \\ π ⊨ φ U ψ & ⟺ & \exists k \geq 0 : π^{k} ⊨ ψ \land \forall j < k : π^{j} ⊨ φ \end{array}

安全性性质说坏事永不发生（ $G \neg crash$ ）；活性性质说好事终将发生（ $G (req \to F grant)$ ）。Clarke 与 Emerson 提出的计算树逻辑（CTL）则对分叉的未来做量化： $AG φ$ 表示在所有路径上始终成立； $EF φ$ 表示在某条路径上终将成立。两种逻辑互不包含；CTL* 同时包含两者。

模型检测

谁、何时。Edmund Clarke 与 E. Allen Emerson（1981 年的工作，1982 年发表）[7]，以及独立工作的 Jean-Pierre Queille 与 Joseph Sifakis（1982）[8]。三人分享了 2007 年图灵奖，获奖理由是“他们在把模型检测发展为一种在软硬件行业中被广泛采用的高效验证技术方面所起的作用”。

是什么。给定系统的一个有限模型，即 Kripke 结构 $M = (S, S_{0}, R, L)$ （状态、初始状态、迁移和状态标签），以及一条时序公式 $φ$ ，自动判定是否 $M ⊨ φ$ ：即从初始状态出发的每条执行是否都满足 $φ$ 。若否，给出一条反例执行。

算例：在一个小系统上检查 LTL 性质。一个有三个状态的资源仲裁器： $s_{0}$ 空闲， $s_{1}$ 标有 $req$ ， $s_{2}$ 标有 $grant$ ；空闲状态可以一直等待。

S = {s_{0}, s_{1}, s_{2}}, S_{0} = {s_{0}}, R = {(s_{0}, s_{0}), (s_{0}, s_{1}), (s_{1}, s_{2}), (s_{2}, s_{0})}

图 1. 仲裁器。初始状态 s0 可以在自环上永远等待；s1 中的请求之后总是 s2 中的授予。

性质 1： $φ_{1} = G (req \to F grant)$ ，每个请求终将被授予。唯一标有 $req$ 的状态是 $s_{1}$ ，它唯一的后继是标有 $grant$ 的 $s_{2}$ 。所以在每条路径上，位于 $s_{1}$ 的每个位置，下一步就是 $grant$ ；位于 $s_{0}$ 或 $s_{2}$ 的位置则平凡地满足这一蕴涵。结论： $M ⊨ φ_{1}$ 。

性质 2： $φ_{2} = G F grant$ ，授予会无穷多次发生。路径 $s_{0} s_{0} s_{0} \dots$ 永远等待，从未到达 $s_{2}$ 。结论： $M ⊭ φ_{2}$ ，模型检测器把这条套索形状的路径作为反例返回。这算不算缺陷取决于意图：如果客户端最终必须发出请求，修正办法是加一个公平性假设，而不是改代码。正是反例让这种讨论变得具体。

检测器怎么做。CTL 通过在状态集合上计算不动点来检查，时间与模型规模和公式规模都成线性关系。LTL 的检查方法是把 $\neg φ$ 翻译成 Büchi 自动机，与模型做乘积，再搜索可接受的环；这个问题对公式是 PSPACE 完全的，对模型则是线性的。

今天用在哪里。芯片行业的硬件验证、通信协议、设备驱动和分布式系统设计。Amazon Web Services 的工程师报告说，他们用 TLA+ 规约语言及其模型检测器在 DynamoDB 和 S3 等系统的设计中发现了隐蔽的缺陷 [9]。

局限。状态爆炸问题：状态数随变量和并发组件的数量呈指数增长。接下来三项是应对它的主要办法。

基于 BDD 的符号模型检测

Randal Bryant 的约简有序二元决策图（BDD，1986）为布尔函数提供了一种规范且往往紧凑的表示 [10]。Burch、Clarke、McMillan、Dill 与 Hwang（1990）用它把状态集合和迁移关系表示为公式而非列表，检查了状态数超过 $10^{20}$ 的系统 [11]。NuSMV 等工具都源自这项工作。BDD 仍可能爆炸，并且严重依赖变量顺序。

有界模型检测

Biere、Cimatti、Clarke 与 Zhu（1999）把迁移关系展开 $k$ 步，把“是否存在长度不超过 $k$ 的反例”这个问题交给 SAT 求解器 [12]。它能很快找到浅层缺陷，并随 SAT 求解器的进步而受益；但单靠它只能证明不存在短反例。CBMC 把这一思想用于 C 程序。

SPIN 模型检测器

Gerard Holzmann 于 1980 年在贝尔实验室开始开发 SPIN；它自 1991 年起免费提供，并于 2001 年获得 ACM 软件系统奖 [13]。模型用 Promela 编写，性质用 LTL 表达，SPIN 会生成一个针对具体问题的 C 语言验证器，并用偏序归约和位状态哈希来对抗状态爆炸。

3. 项重写与 Knuth–Bendix 完备化

项重写

是什么。项重写系统是一组有向等式 $l \to r$ 。重写一个项，就是找到一个与某个 $l$ 匹配的子项，把它替换成 $r$ 的相应实例；重复直到没有规则可用，得到范式。有两条性质使它成为判定等式的程序：

终止性：不存在无穷的重写序列。
合流性：一个项重写成两个不同的项时，两者总能再重写到同一个项。

Newman 引理（1942）。一个终止的重写系统是合流的，当且仅当它是局部合流的：每个一步分叉

t_{1} \leftarrow t \to t_{2}

都能汇合。

在终止且合流（收敛）的系统中，每个项恰有一个范式，所以 $s = t$ 能由等式推出，当且仅当 $s$ 与 $t$ 有相同的范式。今天用在哪里。计算机代数的化简器、编译器优化遍、定理证明器内部的等式引擎，以及 Maude 等重写语言。局限。终止性与合流性一般是不可判定的，而且许多有用的理论（例如交换律）根本不存在收敛的定向。

Knuth–Bendix 完备化

谁、何时。Donald Knuth 与 Peter Bendix，《Simple Word Problems in Universal Algebras》，1970 年 [14]。做什么。它试图把一组等式变成同一理论的收敛重写系统。用一个保证终止的约简序给每个等式定向；找出每个临界对，即两条规则重叠并给出不同重写结果的项；如果两个结果的范式不同，就把它们之间的等式作为新规则加入；化简并重复。

算例：群。从三条群公理出发，从左到右定向：

\begin{array}{l} 1. & e \cdot x \to x \\ 2. & x^{- 1} \cdot x \to e \\ 3. & (x \cdot y) \cdot z \to x \cdot (y \cdot z) \end{array}

规则 2 与规则 3 在项 $(x^{- 1} \cdot x) \cdot z$ 上重叠。规则 3 把它重写为 $x^{- 1} \cdot (x \cdot z)$ ；规则 2 再加规则 1 把它重写为 $z$ 。两者都不可再约且互不相同，于是这个临界对产生一条新规则 $x^{- 1} \cdot (x \cdot z) \to z$ 。继续下去，完备化停在十条规则：上面三条、这一条，以及

x \cdot e \to x, e^{- 1} \to e, {(x^{- 1})}^{- 1} \to x, x \cdot x^{- 1} \to e, x \cdot (x^{- 1} \cdot y) \to y, {(x \cdot y)}^{- 1} \to y^{- 1} \cdot x^{- 1}

有了这十条规则，任意两个群表达式是否相等，都可以通过把两者重写到范式再比较来检验：自由群的字问题就这样被机械地解决了。

今天用在哪里。完备化内置于等式定理证明器中；它的不失败变体（Bachmair、Dershowitz 与 Plaisted，1989）不会卡在无法定向的等式上，E 等叠加证明器则把它推广到完整的一阶逻辑。局限。完备化可能失败（某个等式无法定向），也可能永远运行下去，生成无穷多条规则。

4. 抽象解释

抽象解释

谁、何时。Patrick Cousot 与 Radhia Cousot，POPL 1977 [15]。为什么需要它。由 Rice 定理，没有算法能判定任意程序行为的任何非平凡性质。抽象解释接受这一点，并选择安全的一侧：计算所有行为的过近似。如果近似中没有错误，程序就没有错误；如果近似中有错误，分析器就发出警报，而警报可能是误报。

怎么工作。具体的值集合与抽象值之间通过抽象映射 $α$ 和具体化映射 $γ$ 构成的伽罗瓦连接相联系：

α (X) ⊑ a ⟺ X \subseteq γ (a) 可靠性： α \circ F ⊑ F^{♯} \circ α

每个程序操作 $F$ 都有一个过近似它的抽象对应物 $F^{♯}$ ，循环则作为抽象域中的不动点来求解。

算例：符号域。把每个整数抽象为 ${-, 0, +, ⊤}$ 之一，其中 $⊤$ 表示“未知”。对 x := -3; y := x * x; z := x + y： $x \mapsto -$ ；接着 $- \times^{♯} - = +$ ，于是分析器无须运行任何东西就证明了 $y > 0$ ；然后 $- +^{♯} + = ⊤$ ，所以它无法判断 $z > 0$ 是否成立（实际上 $z = 6$ ）。一次除以 $z$ 的运算会触发警报：可靠，但不精确。更丰富的域以代价换取精度：区间、八边形（Miné，2004）、凸多面体（Cousot 与 Halbwachs，1978）。在区间这类有无穷上升链的域上，加宽算子强制循环分析终止，例如从 $[0, 1], [0, 2], \dots$ 直接跳到 $[0, + \infty)$ 。

今天用在哪里。Astrée 出自 Cousot 在巴黎高等师范学院的团队，现由 AbsInt 销售；Airbus 自 2003 年起把它用于包括 A380 在内的多种机型的安全关键软件，AbsInt 报告说在主飞行控制代码上做到了恰好零误报 [16]。Frama-C、Polyspace、IKOS 和 Infer 也运用了同一理论。

局限。每个可靠的分析器都要在误报与代价之间取舍。要在真实代码上达到足够精度，需要针对代码惯用法调校的抽象域；误报泛滥是这类工具被弃用最常见的原因。

5. 基于 SMT 的验证

基于 SMT 的验证

是什么。演绎式验证器把程序及其标注变成验证条件：当且仅当程序满足规约时才有效的公式，如上面的 Hoare 例子。可满足性模理论（SMT）求解器在程序所需的理论（整数、位向量、数组、未解释函数）上判定这类公式。一个公式有效，当且仅当它的否定不可满足。

谁、何时。Greg Nelson 与 Derek Oppen（1979）展示了如何组合针对不同理论的判定过程 [17]。现代 SMT 求解器把这一思想与 SAT 求解器的搜索结合起来。微软研究院 Leonardo de Moura 与 Nikolaj Bjørner 的 Z3（2008）使用最广 [18]；它于 2015 年以 MIT 许可证开源。CVC5 和 Yices 是其他主要的求解器。

算例。Hoare 例子中的验证条件 $x > 10 \to x + 1 > 10$ ，通过在 SMT-LIB 语言中断言它的否定来检查：

(declare-const x Int)
(assert (> x 10))
(assert (not (> (+ x 1) 10)))
(check-sat)   ; 求解器回答 unsat，所以该蕴涵有效

今天用在哪里。微软的验证感知语言 Dafny 把它的验证条件交给 Z3 [19]。Amazon Web Services 的 Zelkova 把访问控制策略翻译成 SMT 公式，回答诸如“这个账户之外有没有人能读取这个存储桶？”之类的问题 [20]。符号执行和有界模型检测器也依赖 SMT。局限。量词和非线性算术使问题不可判定或非常困难；求解器可能回答未知或超时，结果也可能随求解器版本而变。

6. 程序综合

程序综合：问题本身

Alonzo Church 在 1957 年康奈尔大学的符号逻辑暑期研讨班上提出了从逻辑规约综合电路的问题。对程序而言，经典的表述是：给定一个联系输入 $x$ 与输出 $y$ 的规约 $φ (x, y)$ ，找到一个程序 $f$ ，使得

\forall x . φ (x, f (x)) 它是下式的见证： \forall x . \exists y . φ (x, y)

对于永远与环境交互的反应式系统，Pnueli 与 Rosner（1989）给出了这个问题的 LTL 版本 [21]；它是 2EXPTIME 完全的。

演绎式程序综合

谁、何时。Zohar Manna 与 Richard Waldinger，始于《Toward Automatic Program Synthesis》（1971），集大成于《A Deductive Approach to Program Synthesis》（1980）[22]。怎么工作。构造性地证明 $\forall \exists$ 命题，程序就从证明中读出：分情况讨论变成条件分支，归纳变成递归。算例。规约： $\forall a, b . \exists z . z \geq a \land z \geq b \land (z = a \lor z = b)$ 。证明按 $a \geq b$ 分情况：此时 $z = a$ 可行，否则 $z = b$ 。抽取出的程序是 max(a, b) = if a ≥ b then a else b，由构造保证正确。同样的思想，即程序即证明，也是 Rocq 从已验证开发中抽取可执行代码的方式。局限。找到证明至少和编写程序一样难，而且这种方法需要完整的形式规约，用户很少具备。

归纳式（基于示例的）综合：FlashFill

谁、何时。Sumit Gulwani，《Automating String Processing in Spreadsheets Using Input-Output Examples》，POPL 2011 [23]。这项技术以 Flash Fill（快速填充）之名进入了 Microsoft Excel。怎么工作。用户为一两行输入想要的输出。综合器在一个小型字符串变换领域专用语言（按词元模式定位的子串、常量、拼接）中，搜索与示例一致的全部程序，紧凑地表示这个集合，再给候选排序，偏好最简单的。从 Alan Turing → A. Turing 和 Grace Hopper → G. Hopper，它大致学到“第一个词的首字母，接“. ”，再接第二个词”，并填完这一列的其余部分。局限。示例不足以确定意图：多个程序都能拟合，排名选出的那个可能在用户从未检查的行上泛化出错。可处理的搜索需要一个狭窄的语言。

草图、CEGIS 与语法制导综合

Armando Solar-Lezama 的 Sketch（2006）让程序员写出带“洞”的程序，再请 SAT 求解器填洞，使程序满足规约 [24]。它的引擎推广了反例引导的归纳综合（CEGIS）：提出一个在有限输入集上可行的候选，请验证器找出一个使它失败的输入，把该输入加入集合，重复。语法制导综合（SyGuS，Alur 等，2013）把问题标准化为一条逻辑规约加一套允许程序的文法，并配有通用格式和年度竞赛 [25]。如今，大语言模型常被用来生成候选程序，而在 CEGIS 式循环中决定保留哪些的，是符号验证器。

7. 已验证软件：CompCert 与 seL4

已验证软件

当证明在证明助手中机械化并与代码一起维护时，上述技术就能扩展到整个系统。有两个项目树立了标杆。

CompCert

一个针对 C 语言大子集的形式化验证优化编译器，由 Xavier Leroy 自 2005 年起主持，在 Coq（现名 Rocq）中编写并证明 [26]。定理是：编译后的代码按源程序语义所规定的方式运行，因此编译器在已验证的阶段中不会引入它自己的错误。这一点为何重要，证据来自测试。Yang、Chen、Eide 与 Regehr 的随机测试工具 Csmith 在主流 C 编译器中发现了 325 个以上此前未知的缺陷；在 CompCert 中，它只在未验证的部分发现了缺陷，并报告说“我们在所有其他编译器中发现的中端缺陷，在这里都不存在” [27]。CompCert 于 2021 年获得 ACM 软件系统奖，并自 2015 年起由 AbsInt 商业销售。

seL4

一个通用操作系统微内核，拥有在 Isabelle/HOL 中机器检查的证明，证明其 C 实现相对于规约在功能上正确；该证明由 Gerwin Klein 及其在 NICTA 的同事于 2009 年完成 [28]。后来的证明延伸到编译后的二进制代码，把编译器从必须信任的部分中移除，并覆盖了完整性和机密性性质。seL4 于 2014 年开源，并被用于 DARPA 面向高可信自主载具的 HACMS 项目。它没有说什么。这些证明针对的是内核相对于其硬件模型的行为；错误的规约、硬件故障或内核之外的代码，都在定理之外。

8. 时间线

形式化验证与程序综合，1957 至 2021 年。年份为发表、发布或完成的年份。
年份	技术或系统	人物
1957	提出电路综合问题	Church
1967	流程图上的断言	Floyd
1969	Hoare 逻辑	Hoare
1970	Knuth–Bendix 完备化	Knuth、Bendix
1971	走向自动程序综合	Manna、Waldinger
1975	最弱前置条件、守卫命令	Dijkstra
1977	程序的时序逻辑；抽象解释	Pnueli；Cousot、Cousot
1979	协作判定过程	Nelson、Oppen
1980	演绎式程序综合	Manna、Waldinger
1981–82	模型检测、CTL	Clarke、Emerson；Queille、Sifakis
1986	约简有序 BDD	Bryant
1989	基于 LTL 的反应式综合	Pnueli、Rosner
1990	符号模型检测	Burch、Clarke、McMillan、Dill、Hwang
1991	SPIN 免费发布	Holzmann
1999	有界模型检测	Biere、Cimatti、Clarke、Zhu
2002	分离逻辑（LICS 论文）	Reynolds、O’Hearn 等
2003	Astrée 在 Airbus 投入使用	Cousot 等；Airbus
2006	Sketch 与 CEGIS	Solar-Lezama 等
2007	模型检测获图灵奖	Clarke、Emerson、Sifakis
2008	Z3	de Moura、Bjørner
2009	seL4 证明；CompCert 综述刊于 CACM	Klein 等；Leroy
2011	FlashFill	Gulwani
2013	语法制导综合	Alur 等
2015	Infer 开源；AWS 使用 TLA+ 的报告	Calcagno 等；Newcombe 等
2018	基于 SMT 推理云访问策略	Backes 等

9. 形式化方法做不到什么

针对错误的规约做验证。证明表明代码符合规约。如果规约错误或不完整，证明认证的就是错误的东西。
逃离不可判定性。Rice 定理意味着每个自动工具要么限制它能处理的程序，要么做近似（带误报），要么限定搜索范围，要么可能回答未知。
一般地战胜状态爆炸。符号表示、抽象和有界化推动了边界，但没有消除它。
信任它们自己。每个结果都依赖一个可信基：证明检查器、求解器、硬件或环境的模型。让这个可信基保持小而且经过检查，是这门学科的一部分。
廉价。完整的功能验证仍然要付出数倍于编写代码的工作量。轻量级的用法，比如对设计做模型检测，或证明不存在运行时错误，才是工业回报的主要来源。

学习模型正从两端进入这个领域：作为不变式、证明和候选程序的生成器，也作为本身需要验证的系统。两者的结合是神经符号 AI 的主题。

10. 与失效安全模型的关系

可靠的静态分析器，正是按照失效安全模型应有的行为方式构建的。当 Astrée 无法证明一次除法安全时，它不会猜测“大概没问题”，而是发出警报。可靠性是对系统向哪一侧出错的承诺：出错时偏向一个用户可以检查的拒绝，而绝不偏向悄无声息的放行。模型检测补充了第二个值得借鉴的习惯：否定的结论附带证据，即一条具体的反例路径，而不是一个孤零零的分数。

程序综合提供了第三种模式。在 CEGIS 中，以及在当前由语言模型提议代码的系统中，提议者可以是任何东西；决定保留什么的是验证器。失效安全模型把同样的分工用于事实和动作：模型可以提议；只有地板能接纳一条事实。附带的告诫也同样适用：接纳检查的好坏，取决于它据以检查的东西，这就是为什么每条被接纳事实背后的来源与检查本身同样重要。

Perslis Research 的 Peel，据我们所知，是第一个失效安全模型。Peel 中的知识是有类型、有来源的卡片，学习是可读的计数，在做决定的环路中没有神经网络。Peel 是研究原型，并非经过认证的安全系统。关于为什么跨越多个模型的链条上的不变式需要模型之外的符号层，见我们的论文 The Orchestration Gap [29]；关于基于这一原则构建的流水线模式，见符号流。

11. 常见问题

什么是形式化验证？: 形式化验证是用数理逻辑证明一个程序或硬件设计对每一种可能的输入或行为都满足精确的规约。测试只检查部分情况，而一次完成的验证覆盖全部情况，前提是相对于所用的规约以及被验证的系统模型。
什么是 Hoare 逻辑？: Hoare 逻辑由 C. A. R. Hoare 于 1969 年提出，是一套建立在三元组 {P} S {Q} 之上的程序证明系统：如果命令 S 执行前前置条件 P 成立且 S 终止，则执行后后置条件 Q 成立。它的规则涵盖赋值、顺序、条件和循环；循环需要不变式。它是现代演绎式程序验证器的基础。
什么是模型检测？: 模型检测是一种自动技术，它通过遍历状态来判定一个系统的有限状态模型是否满足一条时序逻辑性质。如果性质不成立，模型检测器会给出一条反例执行。它由 Clarke 与 Emerson 以及 Queille 与 Sifakis 在 20 世纪 80 年代初提出，三人因此获得 2007 年图灵奖。
LTL 和 CTL 有什么区别？: LTL 即线性时序逻辑，描述单条执行的性质，例如 G(req → F grant)：在每次运行中，每个请求终将被授予。CTL 即计算树逻辑，对分叉的未来做量化，例如 EF grant：从这里出发，存在某条执行能到达授予。两者各自能表达对方无法表达的性质；CTL* 同时包含两者。
什么是抽象解释？: 抽象解释由 Patrick Cousot 与 Radhia Cousot 于 1977 年提出，是一套可靠静态分析的理论。它在抽象值（例如符号或区间）上运行程序，这些抽象值过近似了每一次真实执行。如果近似显示没有错误，程序就没有错误；否则分析器发出警报，而警报可能是误报。
什么是程序综合？: 程序综合是根据规约自动构造程序。演绎式综合从“规约可以被满足”的构造性证明中抽取程序；归纳式综合，例如 Excel 的 Flash Fill，在受限语言中搜索与输入输出示例一致的程序；语法制导综合把逻辑规约与文法结合起来。
SMT 求解器在验证中有什么用？: 验证器把程序及其规约变成称为验证条件的逻辑公式。Z3 等 SMT 求解器在整数、位向量、数组等理论上判定这些公式是否可满足。当一个条件的否定不可满足时，该条件就被证明有效；否则求解器通常会返回一个反例。
形式化验证是否意味着软件没有缺陷？: 不是。它意味着软件在所述假设下满足其规约。缺陷仍可能存在于规约、未验证的组件、硬件或被信任的工具中。即便如此，对已验证的 CompCert 编译器进行随机测试，在其已验证部分中没有发现错误代码生成的问题，这正是人们愿意付出这份努力的原因。

12. 参考文献

C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10):576–583, 1969. doi:10.1145/363235.363259.
R. W. Floyd. Assigning Meanings to Programs. Proceedings of Symposia in Applied Mathematics 19:19–32. American Mathematical Society, 1967.
E. W. Dijkstra. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM 18(8):453–457, 1975. doi:10.1145/360933.360975.
J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS), 55–74, 2002.
C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer, M. Luca, P. O’Hearn, I. Papakonstantinou, J. Purbrick, D. Rodriguez. Moving Fast with Software Verification. NASA Formal Methods, LNCS, 3–11. Springer, 2015.
A. Pnueli. The Temporal Logic of Programs. 18th Annual Symposium on Foundations of Computer Science (FOCS), 46–57, 1977. doi:10.1109/SFCS.1977.32.
E. M. Clarke, E. A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In D. Kozen (ed.), Logics of Programs, LNCS 131, 52–71. Springer, 1982. doi:10.1007/BFb0025774.
J.-P. Queille, J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. International Symposium on Programming, LNCS, 337–351. Springer, 1982. doi:10.1007/3-540-11494-7_22.
C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, M. Deardeuff. How Amazon Web Services Uses Formal Methods. Communications of the ACM 58(4):66–73, 2015. doi:10.1145/2699417.
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8):677–691, 1986.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang. Symbolic Model Checking: 10²⁰ States and Beyond. Fifth IEEE Symposium on Logic in Computer Science (LICS), 1990. doi:10.1109/LICS.1990.113767.
A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, 193–207. Springer, 1999.
G. J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5):279–295, 1997.
D. E. Knuth, P. B. Bendix. Simple Word Problems in Universal Algebras. In J. Leech (ed.), Computational Problems in Abstract Algebra, 263–297. Pergamon Press, 1970.
P. Cousot, R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POPL), 238–252, 1977. doi:10.1145/512950.512973.
AbsInt. Astrée: Fast and Sound Runtime Error Analysis. Product documentation, absint.com/astree. Accessed 2026-09-26.
G. Nelson, D. C. Oppen. Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2):245–257, 1979. doi:10.1145/357073.357079.
L. de Moura, N. Bjørner. Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963, 337–340. Springer, 2008. doi:10.1007/978-3-540-78800-3_24.
K. R. M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), LNCS, 348–370. Springer, 2010.
J. Backes, P. Bolignano, B. Cook, C. Dodge, A. Gacek, K. Luckow, N. Rungta, O. Tkachuk, C. Varming. Semantic-Based Automated Reasoning for AWS Access Policies Using SMT. Formal Methods in Computer Aided Design (FMCAD), 1–9, 2018. doi:10.23919/FMCAD.2018.8602994.
A. Pnueli, R. Rosner. On the Synthesis of a Reactive Module. Proceedings of the 16th ACM Symposium on Principles of Programming Languages (POPL), 1989. doi:10.1145/75277.75293.
Z. Manna, R. Waldinger. A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems 2(1):90–121, 1980. doi:10.1145/357084.357090. See also Toward Automatic Program Synthesis, Communications of the ACM, 1971. doi:10.1145/362566.362568.
S. Gulwani. Automating String Processing in Spreadsheets Using Input-Output Examples. Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL), 2011. doi:10.1145/1926385.1926423.
A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, V. Saraswat. Combinatorial Sketching for Finite Programs. ASPLOS 2006; ACM SIGPLAN Notices 41(11):404–415, 2006. doi:10.1145/1168918.1168907.
R. Alur, R. Bodík, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, A. Udupa. Syntax-Guided Synthesis. Formal Methods in Computer-Aided Design (FMCAD), 2013. doi:10.1109/FMCAD.2013.6679385.
X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7):107–115, 2009. doi:10.1145/1538788.1538814.
X. Yang, Y. Chen, E. Eide, J. Regehr. Finding and Understanding Bugs in C Compilers. Proceedings of the 32nd ACM Conference on Programming Language Design and Implementation (PLDI), 2011.
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. seL4: Formal Verification of an OS Kernel. Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), 207–220, 2009. doi:10.1145/1629575.1629596.
Perslis Research. The Orchestration Gap: Why Model-Level Alignment Cannot Survive Multi-Model Runtimes. 2026. research.perslis.com/orchestration-gap