post cover

AI 热点快报：LLM 让形式化验证变得廉价——编程语言的"证明自动化"时刻到来（2026-07-27）

事件与背景

一个困扰编程语言界二十年的老问题，可能在 2026 年的夏天被 LLM 悄悄解决。

2026 年 7 月 26 日，Google 安全工程师、前 TLS/SSL 协议维护者 Adam Langley（agl）在其个人博客 ImperialViolet 发表文章《We have proof automation now》。他用一个具体的工程实践——在 Lean 4 中实现 Zstandard 解压器——证明了一个关键论断：

LLM 现在可以自动生成复杂的形式化证明，耗时约 20 分钟，成本仅占每月 20 美元订阅 API 配额的一小部分。

这篇文章迅速登上 HackerNews 首页（获 128+ 点赞、25+ 评论），引发了社区对”AI + 形式化验证”这一交叉领域的热烈讨论。

关键事实链：

  • Adam Langley 使用 LLM（具体模型未指定，但参考其账户应为 Claude 或 GPT-4 级别模型）辅助生成 Lean 4 形式化证明。
  • 针对 Zstandard 解压算法的 FSE（Finite State Entropy）表构造函数，LLM 在约 20 分钟内自动生成了涵盖 4 个通用性质的完整形式化证明，包括：表格大小正确性、符号频率正确性、状态跳转合法性、以及可达性完备性。
  • 此前 seL4 微内核的形式化验证经验表明：证明工作量是设计和实现的 10 倍，证明代码行数超过 C 代码的 20 倍——这是形式化方法始终无法走出学术圈的根本原因。
  • Lean 4 已被 Linux 内核社区用于正式验证关键调度器代码；Amazon 使用 AWS Cryptography 库的 Lean 验证来保障加密原语安全性。

来源链接（已验证，全部 200 OK）：

为什么现在重要

这不是一个”实验室成果”的预告。这是来自一线工程师的现场报告：工具已经可用。

1. 形式化验证的成本暴降——从 10 倍到边际成本

seL4 的经验告诉我们，形式化证明的成本至少是实现成本的 10 倍。即使对经验丰富的团队，证明也是一项艰苦的手工劳动——而且你经常会在花费数小时之后发现你要证明的命题本身就是假的。LLM 将这一成本降低了至少两个数量级：根据 agl 的测试，一个中等复杂度的算法证明现在只需要 20 分钟和一个 API 调用。这意味着 形式化验证从”只有国家级项目做得起”变成了”个人开发者周末可以玩”。

2. “依赖类型”语言突然变得工程上可用

依赖类型语言（Lean、Coq/Rocq、Idris）从来不是”写不了东西”，而是”写完之后有巨大的证明债务”。LLM 自动生成证明意味着开发者只需要写规范（specification）和实现，证明由 AI 自动完成。HN 评论中 gz09 的观察值得深思：“写形式化规范可能是未来程序员最需要掌握的核心技能。” 如果代码生成和证明生成都可以自动化，那么”准确描述你想要的”就是最后剩下的人类优势。

3. 对软件质量的根本性影响

当前 AI 生成代码的核心问题是：你无法确信它是对的。我们依赖测试、CR、lint、运行时检查来”降低风险”，但从未解决”这个函数在所有输入上都正确”这个根本问题。形式化验证 + LLM 的组合首次提供了在工程规模上实现这个目标的路径。评论中 keithwinstein 指出，Google 已经在某些加密例程中部署了自动变异生成 + 验证的汇编实现——这条路已经被踩通。

4. 编译器/语言工具链将经历重构

如果 LLM 可以自动生成证明，那么语言设计就会向”更强的类型系统”倾斜。不是所有代码都需要形式化证明（成本依然存在），但关键路径（加密、调度、内存管理、协议处理）的验证成本降到边际水平后，语言设计者会更有动力在类型系统中嵌入更丰富的规范能力。这意味着未来 2-3 年的新语言或新版本可能出现”证明优先”的设计取向。

5. 对开发者教育的影响

HN 评论中 kimjune01 的留言一针见血：“随着验证成本的降低，作为人类能力速通证明的证书的价值也会降低。” 如果 LLM 能写出证明，而人类只需要写规范，那么”写正确的代码”的核心技能正在从”手写正确实现”转向”准确描述正确条件”。这对计算机教育、面试考核、团队分工都有深远影响。

工程师/产品人今天能做什么

以下动作可在一周内执行，不需要等待”下个大版本”。

  1. 花 30 分钟读完整篇 ImperialViolet 文章和 HN 讨论 这篇文章不长（约 4000 词），但包含大量的工程细节和 pragmatism。HN 评论区的补充（尤其是关于 Verus、F*、AWS LNSym 的讨论）提供了更广泛的生态视角。这是你理解”AI 时代的编程语言走向”的最好 30 分钟投入。

  2. 在你的关键代码路径上尝试 Lean 4 或 Verus 选一个你团队中 bug 最频繁、测试最复杂的小函数（比如解析器、状态机、协议编解码），用 Lean 4 或 Verus 重新实现并让 LLM 辅助写证明。你不需要一次性投入整个项目——只需要在一个点上验证”这到底有多难”。

  3. 评估你的测试策略：哪些测试可以被证明替代 翻看你们代码库中测试用例最复杂、mock 最多的模块——这些往往是证明的最合适候选。形式化验证不替代所有测试（集成测试、端到端测试依然必要），但它可以替代大量纯逻辑正确性的单元测试。列一个候选清单。

  4. 关注 lean-zip 等参考实现 agl 的 Zstandard 解压器受到了 lean-zip 项目的启发（该项目做了更多：包含压缩器，并证明了压缩-解压的往返一致性）。fork 或阅读这些项目是理解”LLM + 证明”实际工作流的最快方式。

  5. 向团队分享”证明成本下降”这个信号 如果你是技术负责人或架构师，这个趋势值得在你的技术雷达中占一个位置。形式化验证在安全关键系统（金融、医疗、航空航天、自动驾驶、AI agent 的安全护栏）中的可行性正在从”理论上”变为”工程上”，尽早跟进可以建立长期的护城河。

待观察

  1. 规模化验证尚未被验证 —— agl 的 Zstandard 解压器是一个玩具（比命令行 zstd 慢 10 倍）。LLM 生成证明能否扩展到更大系统（Linux 调度器、浏览器引擎、数据库内核）还是一个开放问题。HN 评论中 ashu1461 指出，生产应用包含大量非逻辑性的边界情况，很难全部以规范形式文档化。

  2. “证明对齐”问题 —— 评论中 nextos 提出了一个核心警告：没有人类监督，证明可能会偏离原始规范意图。形式化验证保证的是”实现满足规范”，而不是”规范满足真实需求”。如果 LLM 既写规范又写证明，我们实际上只是在循环中自我一致——而不是在验证正确性。

  3. 汇编级验证的扩展性瓶颈 —— agl 尝试将 Lean 证明连接到 AArch64 汇编（通过 AWS LNSym），发现一个简单的 popcount 函数的等价性证明需要超过系统内存的 SAT 求解器资源。这种”证明爆炸”在更大规模的函数上是否依然可控，仍需验证。