2009年，澳大利亚一群操作系统研究员启动了一个“疯狂”的项目：用数学证明一个微内核操作系统没有bug。他们花了2.2人年写出代码，然后花了20人年去证明它是对的。证明代码量是C代码的20倍，11万行证明对应5700行实现。这个项目叫seL4，在接下来的十几年里，它一直是形式化验证领域的“珠穆朗玛峰”。所有人都知道它是正确的，但没有人能再承受一次这样的成本。
2026年7月，Google安全工程师Adam Langley发布了一篇博文，标题平静得几乎不像一个宣言：《We have proof automation now》。他用Lean 4语言写了一个Zstandard解压器，然后用LLM自动生成了它的全部正确性证明。成本是“每月20美元订阅费的一小部分”。他说，LLM让证明的速度快到了“几乎不需要考虑证明工程”的程度。
如果说seL4是形式化验证的“手工时代”，那么现在，我们可能正站在它的“自动化时代”门口。
两个信号，一个方向
两个几乎同时出现的事件，从不同方向指向同一个结论。
第一个信号来自学术界。2025年，DeepMind的AlphaProof在Nature上发表论文，宣布在IMO 2024上拿到银牌，用Lean证明了3道非几何题，包括全场最难的第6题。这道题在609名人类选手中只有5人做对。AlphaProof通过强化学习训练了8000万道形式化数学问题，在推理时通过测试时RL生成数百万个变体来寻找证明路径。数学证明自动化从“不可能”变成了“可发表”。
第二个信号来自工程界。Kim Morrison（Lean核心贡献者）的lean-zip项目，在GitHub上积累了超过1600次提交，用纯Lean实现了一个完整的DEFLATE编解码器，并由AI自动生成了“编码和解码互为逆运算”的形式化证明。这意味着对于任意输入，压缩不会损坏你的数据。Lean内核验证了全部1100多个定理、约32000行证明代码，没有一个“抱歉”（sorry，Lean中表示未完成的占位符）。而更令人震惊的是，lean-zip的整个实现和验证，全部由AI完成。
然后Adam Langley把这件事又往前推了一步。他选的不是DEFLATE，而是Zstandard。这是一个正在取代gzip成为下一代标准压缩算法的现代方案，由Yann Collet基于Jarek Duda的非对称数字系统（ANS）设计，压缩比与gzip相当，但解压速度快了数倍。它已经被Linux内核、Python标准库（PEP 784）、Chrome、Cloudflare等广泛采用。Langley选择Zstandard不是因为它是“玩具”，恰恰相反，它是有真实工程需求的、复杂的、在生产环境中大规模使用的算法。
他实现了Zstandard解压器中最复杂的部分，基于FSE（有限状态熵）的熵编码器。然后，他让LLM为每一个函数生成了正确性证明。Lean的类型检查器逐一验证，全部通过。
形式化验证的“成本诅咒”
形式化验证有一个根本性的问题：它太贵了，贵到没有一个商业团队愿意承担。
seL4的数据是教科书级别的警示。20人年的证明工作量，2.2人年的实现工作量。每写一行C代码，就要写大约20行证明代码。而且这不是因为工程师不够熟练。seL4团队在项目过程中积累了大量的经验，但证明效率仍然远低于编码效率。
F*语言试图用SMT求解器自动处理证明义务，但这套方案有自己的问题。Langley在博文中形容SMT求解器是一个“复杂而善变的神”。你永远不知道它什么时候会陷入无限循环，跑上几个小时，让你不确定它是在思考还是已经死机。重度用户不得不培养一种“第六感”，去判断什么能让求解器满意。这本质上把证明变成了一种玄学。
为什么LLM恰好是解药
Langley在博文中点出了一个关键洞见，它解释了为什么LLM和形式化验证是天作之合。
在依赖类型系统中，存在一个叫做证明无关性（proof irrelevance）的性质。简单来说，一旦一个命题被证明是正确的，证明的具体内容就不重要了，重要的是“存在一个证明”。这个性质意味着，你不需要给出“优雅的”“可读的”“结构化的”证明，你只需要给出“正确的”证明。
这正是LLM擅长的事情。LLM不擅长构造极其精巧的数学证明，那是人类数学家的领域。但LLM非常擅长“猜”出一个正确的证明路径，然后让类型检查器去验证它。如果错了，重新猜。这个过程可以非常快，因为LLM的推理成本远低于人类专家的时间成本。
Langley的实验证实了这一点。他让LLM生成证明，偶尔需要调整代码风格，比如减少使用命令式风格的Id.run，因为那对证明工具更难处理。但整体上，LLM生成的证明通过了类型检查器。而且，他提到LLM的成本是“每月20美元订阅费的一小部分”。他说“明年这大概会成为标配开销”。
更关键的是，这解决了seL4团队遇到的那个“证明工程”问题。当代码变更时，传统证明需要重新对齐，这是证明维护成本的大头。但如果证明可以自动重新生成，那么“对齐”的成本就趋近于零。
基础设施正在就位
形式化验证的“着陆”其实在2025年就已经开始了。Lean 4在2025年发布了12个版本，从4.15到4.26，带来了数千项改进，其中大量集中在证明自动化上。Lean FRO（形式化研究组织）发布了第三年路线图，将软件验证列为重点方向。AWS的LNSym项目为AArch64指令集构建了形式化语义和模拟器，让处理器级别的验证成为可能。VeriSoftBench发布了500个Lean软件验证基准测试，让LLM的证明能力有了可量化的评估标准。
但真正改变游戏规则的，是LLM推理成本的大幅下降。2025年到2026年，AI价格战将前沿模型API成本压低了90%以上。Claude的价格从每百万token 60美元降到了1到2美元，GPT-5 nano的输入价格仅为每百万token 0.05美元。当证明的“生产成本”从“一个专家的一天”变成“一个LLM调用的一分钱”，形式化验证的经济学就彻底改变了。
lean-zip和Langley的zstd验证是两个“最小可行证明”案例。它们证明了：我们不需要等到LLM完美，不需要等到它能构造出优雅的数学证明，只需要它“足够好”。好到能在合理时间内生成一个通过类型检查的证明。
局限依然存在
Langley的zstd解压器没有发布代码。他给出的理由很诚实：“对于这样一个小的、边界明确的情况，LLM可能做得比我更好。”他的实验只覆盖了解压路径，没有包含压缩器，也没有证明双向往返。此外，纯Lean实现的解压器比命令行zstd慢了10倍。Lean是高级语言，不适合底层性能优化。
更值得警惕的是，lean-zip的验证虽然被证明是“正确的”，但有人在Lean运行时中发现了一个堆缓冲区溢出。这个bug不在已验证的代码中，而在Lean运行时本身。这提醒我们，形式化验证不能消除所有bug，它只是把“bug可能出现在哪里”的边界推得更远，而不是消除它。
这意味着什么
形式化验证的门槛正在从“不可能”降到“昂贵”，再降到“合理”。如果LLM驱动的证明自动化继续以当前速度进步，未来几年内，我们可能会看到形式化验证从“关键系统专享”变成“核心模块标配”。
与此同时，“用Lean写代码，用LLM写证明”可能成为一种新的编程范式。Langley在博文的附注中尝试了这条路径：使用LNSym证明优化后的AArch64汇编实现与Lean函数等价，然后使用汇编代码获得性能，同时保留正确性保证。虽然受限于SAT求解器对某些函数的规模爆炸，但极小的函数已经可以工作。
形式化验证的“范围”和“深度”之间的取舍将变得更加突出。你可以验证整个解压器，但只能覆盖部分属性；你也可以验证一个函数的全部属性，但无法覆盖整个系统。Langley的zstd验证选择了前者，验证了核心熵编码器的正确性，但没有覆盖压缩路径或往返保证。
受益者很清楚：所有需要高可靠性的软件系统，包括加密库、协议实现、文件系统、编译器、区块链节点。如果这些系统的核心组件能用Lean加LLM验证，它们的bug率将大幅下降。
危险者也同样清楚：传统“测试驱动”的质量保障模式。不是测试不重要，而是测试再也无法提供“足够”的保障。当你的竞争对手可以用形式化方法证明他们的代码是正确的，而你还在靠“覆盖率90%”来声称质量，这种差距会越来越难以弥合。
如果你是一个软件工程师，现在可能是时候开始关注Lean了。不需要成为形式化验证专家，但至少要理解“LLM加证明助手”这个组合能做什么、不能做什么。未来两年内，这个能力可能会像“单元测试”一样成为工程团队的标配。
形式化验证从“20人年”到“一个周末”的跨越，不是渐进式的改良，而是成本结构的断裂。当证明的成本从“人力”变成“算力”，唯一限制我们写出正确代码的，就只剩下我们愿不愿意花那20美元了。
快报