随着AI越来越多地参与软件开发，关键问题在于如何验证AI生成代码的正确性和安全性。目前谷歌、微软等企业已有大量代码由AI生成，但缺乏有效的验证机制，这可能导致潜在风险。

当AI开始编写全球软件，谁来确保其正确性？

随着AI技术迅猛发展，软件行业正经历一场革命性变革。Code Metal获得1.25亿美元融资用于AI重写国防工业代码；谷歌和微软报告其25%-30%的新代码由AI生成；AWS用AI为丰田现代化4000万行COBOL代码。微软CTO预测，到2030年95%的代码将由AI生成。这场软件重写浪潮已势不可挡。

然而，验证环节却出现严重缺口。Anthropic用两周时间、2万美元成本开发出10万行C语言编译器，能启动Linux并编译SQLite等主流软件，但无人能证明该编译器的正确性。当AI代码"足够好"时，人类往往停止仔细审查——近半数AI生成代码无法通过基础安全测试，而新型大模型并未显著提升代码安全性。

这种验证缺失可能带来灾难性后果： 1. 历史教训：OpenSSL的Heartbleed漏洞暴露数百万用户隐私通信，经过两年代码审查仍未被发现，最终造成数亿美元损失 2. 规模风险：AI以人类千倍速度生成代码，而现有防御机制（代码审查、测试等）与漏检Heartbleed时并无本质改进 3. 系统性威胁：当AI编写金融系统、医疗设备等关键基础设施时，未经验证的代码将成为系统性风险

更严峻的是，攻击面正在转移：通过污染训练数据或入侵模型API，攻击者可将精心设计的漏洞注入AI接触的每个系统。传统代码审查难以检测这类刻意隐藏的漏洞。

解决方案在于形式化验证——用数学证明确保代码正确性。其核心优势包括： - 全面覆盖：一个证明涵盖所有可能输入和边缘情况 - 不可欺骗：测试策略可能被针对性绕过，但数学证明无法作弊 - 硬件级验证：能捕捉时序侧信道等测试无法发现的底层问题

验证平台需要具备以下特征： 1. 小型可信内核：仅数千行代码机械检查每个证明步骤 2. 开源与独立性：验证系统必须独立于代码生成AI 3. 统一环境：集成编程语言与定理证明器，消除转换间隙 4. 丰富知识库：数学证明与软件验证本质相通 5. 深度可扩展性：支持用户和AI构建自定义工具

目前，Lean平台已成为AI形式化验证的事实标准： - 被Google DeepMind等顶级AI团队采用 - 拥有史上最大形式化数学库Mathlib（20万定理） - AWS已用于验证Cedar授权引擎 - 微软用于验证SymCrypt加密库

实际案例验证了可行性：研究人员用通用AI（未经专门训练）将广泛使用的zlib压缩库转换为Lean版本，并完成机器验证证明。关键定理证明了解压缩总能还原原始数据，这是测试永远无法提供的绝对保证。

未来图景已然清晰：从加密库到SQLite，从协议实现到编译器运行时，关键软件栈将逐层重建并内置数学证明。验证组件将成为永久公共品，其优势将呈超线性扩展——系统越复杂，验证与测试的差距越显著。

工程师的角色将转向更高层次： - 更多精力用于编写规范与模型 - 精确定义系统必须满足的不变量 - 设计先于生成，思考先于构建

这场变革不仅是技术升级，更是信任基础设施的重构。当AI能生成可证明正确的代码时，它就从生产力工具蜕变为可信基石。问题的核心不再是AI能否编写软件，而是我们能否证明这些软件的正确性。

（注：本文在保留原文核心论点和关键案例的基础上，对技术细节进行了适当简化，删减了部分企业背景介绍和平台推广内容，使主题更加聚焦于AI软件验证的必要性与实现路径。）

以下是评论内容的总结，平衡呈现不同观点并保留关键引用：

支持AI代码验证的观点

1. 形式化验证的必要性

   • Leonardo de Moura提出，随着AI生成代码比例增加，必须采用机器检查的形式化验证（如Lean平台），将重点从调试转移到精确规范（评论1）
   • "The only sustainable path forward is machine-checked formal verification"
   • 未来关键软件栈将重构为内置数学证明（评论15）

2. AI验证的演进趋势

   • AI最终将通过生成过程验证（如代理循环跟踪）和自检环境实现自我验证（评论14/20/25）
   • "The software is going to verify itself eventually"（评论25）
   • 新工程范式更关注结构完整性而非代码生产（评论12）

质疑AI验证有效性的观点

1. 基础能力不足

   • 当前AI仍频繁生成错误代码，开发者甚至不阅读就提交（评论5/8）
   • "still does a lot of basic idiotic stuff"（评论8）
   • 形式化验证无法解决未定义规范的创新问题（评论6）

2. 人类理解不可替代

   • 关键系统仍需人类深度理解以承担责任（评论7）
   • "The bottleneck is how fast humans can construct their understanding"
   • 数学验证可能证明错误命题（评论19/30）

中间立场

1. 工具辅助方向

   • Dafny等折中方案比Lean更实用（评论11）
   • AI可优化代码可审查性（评论17）
   • "training wheels are still mandatory"（评论8）

2. 行业现实挑战

   • 需重大事故才能唤醒对速度代价的认知（评论3）
   • 未经测试的AI生成代码可能通过合规审查（评论4）
   • 敏捷开发可能回归更重设计（评论24）

极端观点

• 悲观派认为文明将因不可验证的AI系统崩溃（评论21）
• 乐观派预测未来源码将是提示词序列（评论16）

关键分歧点：形式化验证的可行性（评论1 vs 21）、人类角色的存续（评论7 vs 12）、技术成熟度时间表（评论3 vs 16）。