AI 推动形式化验证走向主流，初创公司数量激增

AI 正在让形式化验证走向主流……这是我 2025 年 12 月写下的，嗯，经过过去 12 个月，我觉得很难再反驳这一点。AI 确实让形式化验证走向了主流。不仅形式化验证初创公司数量暴涨，Claude 还在单个验证项目中写了十亿行 Rocq，从 Claude Code 的创造者到 Vercel CEO、Codex/Cursor 的主要开发者，人人都在谈论形式化验证。早期初创公司除了产出数学证明之外，已经开始在软件上展现经济价值：Theorem 与 Anthropic 合作的二进制验证工作、Harmonic 对 C 程序和硬件设计的验证……随着网络安全风险飙升，形式化验证不仅变得更简单，经济价值也在提升。

人们现在问的问题不再是「我们如何证明 X」，而是「关于 X 我们能证明什么」；或者「还有什么我们证明不了」？这些都是好问题，我写这篇文章一部分是为了回答它们；另一部分是作为去年那篇《测试，而不要（只）验证》的续篇。先剧透结尾：我对形式化验证非常乐观，但我认为当人们说某个东西「经过形式化验证」时，他们所指的东西千差万别，我会试着拆解成我乐观和悲观的部分。

从标题说起。我是 SF 圈子里所说的「可验证性信仰者」（verifiability-pilled），我长期以来（嗯，两年了）一直主张，可验证性是 AI 能给我们带来多少杠杆的极限；我粗略的长期观点是，我们会围绕系统中这些可验证组件的尖峰来构建技术栈。如今，一提到可验证性，形式化验证很快就会跳进讨论。然而不知为何，经过形式化验证的系统仍然可能有 bug，当我听到有人说他们对系统做了形式化验证时，我内心并不会涌起对其正确性的信心洪流。另一方面，当有人说他们在系统中发现了一个 bug 时，我相当确信他们确实发现了。我认为这是因为测试是可验证的，它产生一个定义明确、可审查、可理解的对象——一份经典的 bug 报告。测试是可验证的（由人类验证），就像 UI 组件是可验证的一样，这就是为什么两者都非常容易用 AI 来辅助。

而形式化验证则包含「已验证」的组件，这些组件不需要外部审查，即证明本身；以及难以验证的组件：定义本身、我们正在证明其事实的对象底层模型、执行验证的证明器。形式化验证的主张也非常强——形式化验证做出的是全称（forall）断言，测试做出的是存在（exists）断言——任何难以验证的组件中的任何错误，都可能导致证明的崩塌。

让形式化验证更「可验证」有几条路径，最简单的是减少这些可信组件的数量或规模。一个很好的例子是最近的「二进制验证」方法：我们不去证明程序本身的事实，而是证明这些程序编译后二进制的事实。这让我们能够：(1) 省略对高级编程语言语义的建模，转而建模机器语义——想必更简单——同时摆脱对编译器正确性的依赖（这真不是个好主意，编译器有很多 bug）；(2) 避免对不止一种、而是多种高级语言的语义建模，因为源码级验证要求你分别对每种语言建模，而在二进制层面它们都收敛到同一个模型。

然而在我看来，这只解决了问题的一小部分。可信面仍然巨大，你的可信计算基中既有机器语义又有 Linux 进程语义，两者都需要额外验证。但更重要的是，谈论「形式化验证 X」仍然是错误的，准确的说法是「形式化验证 Y 的 X 性质」。这种术语上的区分曾经是一种约定俗成的共识：当我们听到「CompCert 是经过形式化验证的编译器」或「seL4 是经过形式化验证的微内核」时，我们默认作者没有验证空洞或平凡的性质，因为验证工作本身被置于很高的标准之下，而这与研究者声誉高度相关。说我们「默认」了这些，其实是对科学方法和形式化验证社区的巨大不公，因为现实中这些工作经历了广泛的同行评审，人们在其上构建了其他经过形式化验证的系统，而且它们也有过 bug。然而，正如 AI 震动了软件工程中的代码审查，它对证明工程有着类似甚至更激进的效应。如果说 AI 让世界上软件的数量增长了 10 倍，那它可能让世界上「经过形式化验证的软件」数量增长了 1000 倍。这种民主化几乎影响了每个领域的传统验证策略，但一个领域原本越小众，受这种数量变化的影响就越关键。

我认为我们必须尽快废除「经过形式化验证的软件」这一概念，细微差别必须出现。每一场关于形式化验证的讨论都必须附带一串注意事项，精确理解什么是可信的、什么是已证明的、什么不是。其中一些已经在做了：新的 Lean 证明会在「内核可靠性 bug 可能已被 LLM 利用」的可能性下被讨论，comparator 正在成为验证新 Lean 证明的标准工具，像 Anthropic 与 Theorem 的无崩溃验证以及 Google DeepMind 的 Signal 验证这样的重大公告，都会说明证明的局限性以及可信计算基。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）