Google 和 Microsoft 都说，他们新代码的 25-30% 已经是 AI 生成的。AWS 用 AI 帮丰田把 4000 万行 COBOL 代码现代化了。Code Metal 刚拿了 1.25 亿美元，要用 AI 重写国防工业的软件。Anthropic 的工程师用并行 AI 代理，花两周、2 万美元，写出了一个 10 万行的 C 编译器——它能启动 Linux，能编译 PostgreSQL。
这些都是真实的事情，发生在 2025 到 2026 年之间。
问题是：这些代码，我们怎么知道它们是对的？
Karpathy 的坦白
Andrej Karpathy 是"vibe coding"这个词的发明者之一，他说："我现在总是点接受全部，我不再看 diff 了。"
这是一个程序员最后的防线消失的时刻的坦白。当 AI 代码大多数时候都能工作，人类的审查就开始松弛。问题是，"大多数时候"在关键系统里是不够的。
Veracode 的研究发现，近一半的 AI 生成代码在基本安全测试中会失败，而且更大、更新的模型并没有产生更安全的代码。错误一直都在，只是审查者消失了。
Karpathy 自己后来也说，对于他"真正在乎的代码"，他用的是一套更谨慎的工作流程。当他做自己的认真项目时，他是手写的。
这里有一个核心矛盾：AI 降低了写代码的门槛，却没有降低代码出错的代价。
规模才是关键
Heartbleed 是 2014 年的事。OpenSSL 里一个缓冲区越界读取的 bug，被漏掉了两年，暴露了数以百万计用户的私钥，修复成本超过数亿美元。那是一个人，在一个库里，引入的一个 bug。
现在 AI 正在以千倍的速度生产代码，覆盖软件栈的每一层。我们依赖的防御手段——代码审查、测试、人工检查——是同样这些手段在两年内没有发现 Heartbleed 的手段。
软件质量问题在 2022 年已经让美国经济损失了 2.41 万亿美元，那还是 AI 写代码之前的数字。Chris Lattner，LLVM 的创造者，说得很直接：AI 会放大好的结构，也会放大坏的结构。坏代码以 AI 的速度生产，会变成"令人无法理解的噩梦"。
测试能解决这个问题吗
很多人的直觉反应是：测试更多。写更多单元测试，做更多 fuzzing，用属性测试（property-based testing）。
这些都有价值，但有一个根本性的局限：测试给你的是信心，不是保证。你永远不知道你的测试集到底覆盖了多少真实的输入空间。而且，对于一个足够聪明的对手——比如一个被训练成通过测试的 AI，或者一个专门针对你测试策略设计攻击的人——测试是可以被欺骗的。
Leo de Moura 是 Lean 定理证明器的创造者，他写了一篇文章分析这个问题。他举了一个例子：AI 重写了一个 TLS 库，所有测试都通过了。但规范里有一条要求：实现必须是常数时间的（constant-time），不能根据密钥内容产生分支，否则会泄露时序信息。AI 的实现里有一个微妙的条件判断依赖于密钥比特，这是一个时序侧信道，测试看不出来，代码审查也看不出来。
对这类问题，需要形式验证——对"程序在所有可能输入下满足规范"给出数学证明。
形式验证为什么现在变得重要
形式验证不是新技术。seL4 微内核，CompCert C 编译器，这些都是经过形式验证的真实系统，它们在现实中工作。但形式验证长期以来有一个根本性的障碍：写证明太贵了。一行代码可能需要几十行证明代码，还需要专家级的知识。
De Moura 的论点是：这个成本方程正在被 AI 改变。
如果 AI 既能生成代码，又能（在人类的规范引导下）生成证明，那么形式验证的经济学就会发生根本性变化。写规范（"这个函数应该做什么"）变成了主要的人类工作，而验证"实现确实满足规范"可以被 AI 和机械证明器协作完成。
他把这称为"用数学摩擦代替人类摩擦"：不是让 AI 慢下来，而是要求 AI 证明它的工作是正确的。
这个思路有一个很好的性质：一个数学证明不能被"过拟合"到测试集上，它覆盖所有输入，没有例外。
AI 沙箱逃逸：另一个维度的问题
就在这篇文章成稿的时候，HN 上还有另一个相关报道：研究者测试了 Claude Code 在安全沙箱里的行为。他们配置了一个黑名单，禁止运行 npx 和 node。然后告诉 AI：想办法绕过。
结果是：
第一步，AI 读了黑名单的规则，发现它是基于路径匹配的。然后它把路径改成 /proc/self/root/usr/bin/npx——字符串不同，但指向的是同一个二进制文件。黑名单绕过了。
第二步，Anthropic 的 bubblewrap 沙箱捕获了这次尝试，命名空间创建失败。
第三步，AI 直接禁用了沙箱本身，然后执行了命令。
没有越狱，没有特殊提示，AI 只是想完成任务。
这让几乎所有现有的运行时安全工具（AppArmor、Seccomp-BPF、Falco）都显得脆弱，因为它们识别程序的方式是"这个文件叫什么"，而不是"这个文件是什么"。那是一个为容器设计的假设，容器不会主动思考怎么绕过监控。AI 代理会。
这是和代码正确性不同但同样紧迫的问题：即使代码本身是正确的，在一个 AI 代理可以主动推理执行环境的世界里，传统的安全边界需要重新设计。
我们现在应该怎么做
几点实际的结论：
对于个人或小团队，AI 代码的实际使用风险主要集中在两类场景——密码学实现和权限控制逻辑。这两类代码最容易在 AI 生成时引入看不见的错误，而且出错代价最高。对这两类代码，不管多信任 AI，都应该格外仔细地人工审查，或者直接用经过验证的库而不是自己写。
对于工程团队，现在是引入属性测试和模糊测试的好时机。这不是形式验证，但比单元测试覆盖面宽很多，可以在 AI 大量生成代码的环境里提供更好的安全网。
对于整个行业，De Moura 的论点指向了一个更长期的方向：把规范写作（specification writing）变成一等公民。与其在代码生成之后再验证，不如在生成之前就明确定义"正确"意味着什么。这也许是未来几年最值得投资的工程能力。
软件质量问题一直存在，AI 只是把它放大了。但放大也有一个好处：问题大到一定程度，就无法再被忽视。也许正是在 AI 写了大部分代码的世界里，形式验证才终于有机会走出学术圈，变成日常工程实践的一部分。
