Lean 创始人：当 AI 开始写代码，谁来证明它是正确的？
内容提要
Lean创始人Leo de Moura指出，AI生成代码日益普遍，但测试只能发现Bug、无法证明其不存在，因此形式化验证变得关键。AI通过自动形式化大幅降低验证成本，可生成机器可检查的证明，甚至发现真实Bug。未来规格说明、模型与架构约束将成为核心资产，程序员的价值转向定义正确性、设计系统与审查证明，Agent安全边界也需形式化验证。
延伸解读
测试的边界与形式化验证的补位
文章强调测试只能证明Bug存在，无法证明其不存在，因为无法穷举所有输入和状态。形式化验证通过数学证明覆盖所有满足前提的输入，弥补了测试的天然局限。但文章也指出，证明针对的是模型而非原始程序，若模型与实现不一致，证明可能失效。因此，形式化验证并非替代测试，而是与测试、模型一致性检查共同构成更完整的质量保障体系。
AI降低门槛，但模型忠实性仍是关键风险
AI自动形式化大幅降低了编写规格和证明的成本，甚至让不熟悉Lean的开发者也能借助AI发现真实Bug。然而，文章特别提醒：证明一个Lean模型正确，不等于证明原始程序正确。AI在将源代码转换为模型时可能遗漏整数溢出、并发竞争等细节。差分测试和Aeneas等工具可用于建立源代码与模型之间的对应关系，这是采用AI生成证明时必须关注的环节。
规格说明可能成为长期维护的核心资产
当AI能根据需求快速重新生成实现时，代码本身的可维护价值相对下降，而规格说明、系统模型、架构约束和已验证性质成为更稳定的知识载体。文章提出“规格说明仓库”的设想：形式化规格与实现之间建立可机器检查的关系，减少文档与代码脱节的问题。但这要求团队具备定义精确性质的能力，并持续处理需求鸿沟和模型鸿沟。
Agent安全边界需要可信的实现验证
文章将形式化验证延伸到AI Agent的安全领域：沙箱隔离、权限检查、通信协议和长时间运行的状态转换，如果其实现本身存在漏洞，策略再完善也可能被绕过。Lean生态正在发展多个独立实现的证明检查内核，通过交叉检查降低对单一实现的信任依赖。这提供了一种纵深防御思路，但文章也明确，多内核检查并不能消除所有安全风险。
Q&A
为什么说测试无法证明代码没有Bug？
测试只能验证被执行到的场景，即使编写数万个测试用例，也无法穷举所有可能的输入、状态和执行路径。因此测试擅长证明Bug存在，却无法证明Bug不存在。
形式化验证具体是怎么工作的？
形式化验证用数学语言描述程序应满足的性质（规格说明），然后通过数学证明让机器检查程序是否满足这些性质。它包含三个核心概念：规格说明（程序应满足什么性质）、实现（实际运行的程序）、证明（实现满足规格说明的机器可检查证据）。
AI如何降低形式化验证的门槛？
AI通过自动形式化（Autoformalization）将自然语言描述、数学论文甚至已有程序转换成Lean能理解的形式化模型，并生成机器可检查的证明。这大幅降低了过去需要深厚数学基础和专门证明助手知识的高昂成本。
AI生成的Lean证明能直接说明原始程序没有Bug吗？
不能。证明一个模型正确不等于证明原始程序正确。AI根据源代码生成Lean模型时可能错误理解原始程序，例如忽略整数溢出等机器限制，导致模型被证明正确而原始程序仍有Bug。需要关注模型忠实性，可通过差分测试（Differential Testing）比较原始程序和模型的行为来发现不一致。
当AI能写代码后，程序员的核心价值会变成什么？
程序员的价值将向更高抽象层迁移，重点转向编写形式化规格说明、定义程序应满足的性质、建立准确的系统模型、理解和审查AI生成的证明、设计复杂系统的架构与协议，以及判断形式化模型是否真正覆盖现实需求。底层编程能力仍然重要，但价值重心会转移。
为什么说未来最重要的代码可能是规格说明？
因为当AI能够根据规格说明随时重新生成实现和证明时，代码本身可能不再是长期维护的核心资产。真正需要持续维护的是规格说明、系统模型、架构约束和已验证的性质。规格说明成为可检查、持续演进的工程资产，而代码的角色可能转变为规格说明的一种可生成实现。
AI Agent的安全边界为什么也需要形式化验证？
AI Agent能执行真实操作（访问文件系统、执行命令、调用API等），通常用沙箱和权限策略控制。但如果执行安全策略的代码本身有Bug（如路径穿越漏洞、并发竞争），策略再完善也会被绕过。因此沙箱隔离性质、权限检查逻辑、通信协议和授权边界等都需要形式化验证，成为Verified Software Stack的一部分。
