Lean 创始人 Leo de Moura 解析 AI 如何推动形式化验证从理论走向工程实践

AWS VP Leo de Moura 指出，生成式 AI 的突破使形式化验证（Formal Verification）的成本大幅降低，核心变化在于模型具备了将任意编程语言代码或数学论文自动转化为 Lean 证明的能力（Autoformalization）。这一转变让开发者不再依赖人工编写繁琐的证明脚本，而是通过 AI 生成机器可检查的 Proof，从而在 Rust、C++ 等现有代码库上快速建立可信度，甚至能直接用于发现如 Claude Code 中的真实漏洞。

关键细节显示，验证的可信度不再单一依赖 Lean 官方内核，而是通过多个独立实现的验证器（包括用 C#、Haskell、TeX 甚至 COBOL 编写的内核）进行交叉比对，以应对 AI 可能利用内核漏洞伪造证明的风险。同时，软件工程的范式正从“编写代码”迁移至“编写规格”，即要求工程师具备定义精确属性（Properties）和威胁模型的能力，而代码本身可由 AI 根据这些规格生成并附带证明。Mathlib 已扩展至 250 万行，且 AI 生成的证明长度已达数千万行，证明了该路径在数学领域的可行性。

推论认为，未来软件交付的核心资产将是经过形式化验证的规格文档而非源代码本身，这要求 CS 教育体系调整以强化逻辑与规格描述训练。对于 Agent 系统，验证将聚焦于沙箱隔离策略和行为政策的正确性，确保长运行 Agent 不会越权。尽管金融、法律等领域存在主观性或保密性挑战，但形式化验证有望成为高可靠性系统的标准配置，彻底改变“信任代码”的行业惯例。事实：AI 已能自动生成 Lean 证明；推断：规格将成为核心资产；猜测：非科学领域的大规模应用仍需时间。