内容摘要
演讲核心观点是：在 AI 代理生成海量代码的时代，测试、LLM 评审和人工审查都不足以保证“对所有输入都正确”，而形式化验证可以给出数学证明。真正可落地的路径不是让人审代码，而是让人把控规格，让机器负责实现与证明。
关键观点
形式化验证被定位为唯一可证明“全输入正确”的方法
演讲者先建立问题背景：AI 代理正在以前所未有的速度生成代码，传统质量保障手段在规模和确定性上都遇到极限。LLM 评审是概率性的，测试只能覆盖部分输入，人工审查也难以匹配代理生成速度。与之相比，形式化验证的卖点不是“更可能正确”，而是能对所有输入给出数学证明。这使它从经验性保障工具提升为确定性保障工具。
为什么重要: 这直接改变了代码质量治理的上限。对于高风险、高复杂度或安全关键系统，团队可以从“尽量发现 bug”转向“证明某类 bug 不存在”。
支撑证据
None of these can say for all inputs the code is correct. Formal verification can.
规格而不是代码，才是人机协作链条中的上游资产
演讲者强调，规格定义了“正确”的含义，因此它是整个验证流程的源头。无论规格是直接用 Lean 编写，还是先用自然语言描述再由 AI 自动形式化，人都必须认真验证它。因为一旦规格有偏差，下游再完美的实现与证明也只能证明“错的东西被正确实现了”。这使规格从一次性文档变成持续演化的核心工件。
为什么重要: 这为 AI 编码时代的工程职责分工提供了清晰边界：人应主要控制需求与约束，机器负责实现与证明。这样比让人回头海量审代码更可扩展。