介绍如何通过规范驱动开发与 Lean4 等形式化证明工具，从数学层面保证 AI 生成代码的正确性，超越测试或人工审查的能力边界。
AI translation, not an official translation. Refer to the original for technical details.
Adapted from @CoreyGallon@varun_pant_ 提出，目前团队检查 AI 生成代码的各种方式——LLM 作为评判者、测试、人工审查——实际上都无法对每一个输入都证明代码正确。形式化验证可以做到这一点，这正是他在 @aiDotEngineer YouTube 频道上的演讲主题：《Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers》。Varun 在 AWS 构建 AI 产品，目前从事神经符号 AI 方向的研究。他通过真实生产系统案例，逐步讲解了如何从书面规范走向经数学验证的实现。 - 规范在上游，代码在下游。在规范驱动开发中，由人类编写并验证规范（在 Lean 中以形式化方式表达，或以自然语言编写后自动形式化），编码 Agent 负责实现，形式化验证工具则负责证明实现与规范相符。 - Lean 将代码与证明合二为一。不存在单独的证明语言，也不需要翻译层。一个小型可信内核负责检查每一个证明，该内核可以用 C++、Rust 或 Lean 本身独立重新实现并加以验证。 - zlib 被翻译并得到证明。AI 将 C 压缩库 zlib 转换为 Lean，按照先规范、后实现、再证明的顺序进行，最终生成约 32,000 行证明代码。 - Cedar 用 Lean 规范验证 Rust 实现。AWS 的 Cedar 授权策略语言，其规范用 Lean 编写，生产代码用 Rust 编写。每晚运行约 1 亿次差异化随机测试，以确认两者给出相同结果，只有通过验证才能发布新版本。 - Verus 与 Z3 求解器。Rust 代码通过添加"requires"和"ensures"注解来表达前置条件和后置条件，由 Z3 求解器作为静态检查进行验证，这些注解在运行时会被擦除。 - Strata：面向任意语言的统一验证器。AWS 的这一开源在研项目允许你为某种语言定义"方言"，将其降低为基于 Lean 的共享表示，再分发给 Lean 的证明器、SMT 求解器或模型检查器。 我正在逐一整理 AI Engineer World's Fair 已发布的演讲，分享摘要与心得。欢迎关注，获取更多内容！
