Prediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog

AI 将推动形式化验证从边缘学科走向软件工程的主流。长期以来，诸如 Rocq、Isabelle、Lean、F* 和 Agda 等证明辅助工具虽然存在，但主要局限于学术研究或极少数高保障软件领域。

这是因为编写形式化证明极其困难，往往需要博士级的专业知识，且耗时巨大。例如，验证 seL4 微内核曾耗费了 20 人年的工作量。在大多数系统中，修复错误的预期成本低于使用证明技术消除错误的成本，因此工业界很少采用形式化方法。

随着基于 LLM 的编码助手在编写实现代码和证明脚本方面的能力不断提升，这种情况正在发生根本性改变。目前这一过程仍需人类专家的指导，但他预计在未来几年内该过程将实现完全自动化，从而彻底改变形式化验证的经济效益。

如果形式化验证的成本大幅降低，我们不仅可以负担得起验证更多软件的费用，还能有效解决 AI 生成代码的信任问题。相比于人工审查 AI 代码，让 AI 证明其生成的代码符合规范是更安全、更高效的选择。

编写证明脚本是 LLM 的最佳应用场景之一。因为证明检查器（proof checker）本身是经过验证的代码，它会拒绝任何无效的证明，并强制 AI 智能体重试，直到生成正确的证明。这种机制利用形式化验证的精确性抵消了 LLM 的概率性和潜在的幻觉问题，使得 AI 生成的代码比包含人为疏忽的手工代码更值得信赖。这意味着软件开发的挑战将从编写证明转移到正确定义规范上，即确保被证明的属性确实是用户所关心的属性。

Martin Kleppmann 展望未来，认为软件开发的性质将发生转变：开发者只需以高级声明式的方式指定代码属性，然后由 AI 智能体生成实现代码及相应的证明。开发者甚至无需查看 AI 生成的代码，就像现在无需查看编译器生成的机器码一样。

形式化验证成本的降低、AI 生成代码对验证的需求以及验证对 LLM 不确定性的弥补，将共同推动这一技术的普及。Martin Kleppmann 认为，未来的限制因素可能不再是技术，而是人们意识到形式化方法已切实可行的文化观念转变。