人工智能将推动形式化验证技术进入主流软件开发领域。目前形式化验证主要应用于研究项目,工业界较少采用,但AI有望改变这一现状,使开发者能更轻松地为代码编写形式化规范并进行数学证明,确保代码在各种边缘情况下都符合规范要求。

标题：AI将推动形式化验证成为主流——Martin Kleppmann博客观点

核心内容： 1. 技术现状 - 形式化验证工具（如Rocq、Isabelle等）已存在数十年，能通过数学证明确保代码完全符合规范 - 目前仅用于研究项目（如seL4微内核、CompCert C编译器等），工业界应用罕见 - 验证成本极高：seL4案例中每行C代码需要23行证明代码和0.5人日工作量

2. 传统困境

• 需要博士级专业人才（全球仅数百人掌握）
• 验证成本通常高于潜在缺陷成本
• 存在"负外部性"问题：用户而非开发者承担缺陷后果

3. AI带来的变革

• LLM编码助手能编写证明脚本（需专家指导，但未来可能全自动化）
• 验证经济性将彻底改变：成本大幅降低后，可验证更多软件
• AI生成代码更需要形式化验证来替代人工审查

4. 技术优势

• 证明检查器可过滤LLM的无效证明（自验证的小型代码）
• 规范定义仍需要人类专家，但比手动验证更高效
• AI可辅助规范编写，实现形式语言与自然语言转换

5. 未来展望

• 开发模式转变：声明式规范→自动生成带证明的实现
• 三大驱动力：验证成本降低、AI代码需要验证、形式化抵消LLM的不确定性
• 主要障碍将转为文化接受度而非技术本身

（注：已删除原文中关于作者联系方式、赞助请求等非技术性内容，保留核心技术论述和典型案例数据）

以下是评论内容的总结：

支持AI推动形式化验证成为主流的观点

1. 执行与验证机制是关键

   • "确保编码代理能够运行命令执行代码...下一步是良好的自动化测试套件" (simonw)
   • "形式化验证工具可能成为编码代理的强大解锁工具" (simonw)

2. AI降低验证门槛

   • "主流形式化验证不会突然变成人人使用Lean...而是AI将形式化检查悄悄融入现有工作流" (pedrozieg)
   • "当模型容量再次跃升时，我预测它会涌现设计更好的系统" (yuppiemephisto)

3. 特定领域优势

   • "领域特定语言+形式化验证...可以限制输出格式使验证更快" (whazor)
   • "形式化验证在实现比规范复杂得多的领域（如密码学）表现出色" (bkettle)

质疑AI推动形式化验证的观点

1. AI当前局限性

   • "除非你给LLM提供规范...否则它会产生无效的TLA+输出" (henning)
   • "现在：AI生成错误代码。未来：AI生成错误代码及证明该错误行为的形式化验证" (p1necone)

2. 需求变化与敏捷开发的冲突

   • "形式化验证需要固定需求，而现实世界需求不断变化" (Analemma_)
   • "证明从未流行起来是因为软件工程已转向敏捷开发" (jameslk)

3. 人类参与的必要性

   • "你仍然需要人员来指导和理解证明" (agentultra)
   • "如果AI能完成最困难的事，就没有理由假设它不能完成更容易的事" (pron)

中立/其他观点

1. 替代方案建议

   • "高级测试实践（基于属性的测试、模糊测试）是更好的候选方案" (chamomeal)
   • "Rust和Haskell等语言可能通过LLM变得更易访问" (nrhrjrjrjtntbt)

2. 经济因素考量

   • "如果形式化验证能被中间商利用获利，它就会成为主流" (heliumtera)
   • "AI狂热者会喜欢这个，因为这让他们'AI取代所有开发者'的梦想成真" (skeeter2020)

3. 技术发展预测

   • "这属于科幻范畴...没有明确理解AI的难易点前，任何预测都是随意猜测" (pron)
   • "如果需要的技术是'AGI'，那么所有赌注都是开放的" (jacquesm)

关键分歧点：
- 支持方认为AI能降低形式化验证的技术门槛
- 反对方强调需求动态性和AI可靠性问题
- 第三方建议关注测试实践改进或指出经济驱动因素