Anthropic 用一群 AI agent 花两周写了一个 10 万行的 C 编译器，花费不到 2 万美元。它能启动 Linux，能编译 PostgreSQL、Redis、SQLite。
但没有人对这个编译器做过形式化验证。
这不是一个假设性的担忧。这是 Lean 定理证明器的创造者 Leo de Moura 最近发出的警告，而且他给出的数据让人坐不住。
现在到底发生了什么
先看几组数字：
- Google 和 Microsoft 都表示，新代码中有 25-30% 是 AI 生成的
- AWS 用 AI 帮丰田把 4000 万行 COBOL 代码现代化了
- Microsoft CTO 预测到 2030 年 95% 的代码将由 AI 生成
- 一家叫 Code Metal 的公司刚融了 1.25 亿美元，专门用 AI 重写国防工业代码
这不是未来。这是正在发生的事。
问题出在哪
Andrej Karpathy（对，vibe coding 这个词就是他发明的）说了一句大实话：
"I 'Accept All' always, I don't read the diffs anymore."
翻译：我直接全部接受，不看代码差异了。
当 AI 生成的代码「大部分时候」是对的，人类就会停止仔细审查。这是人性。你试试每天看 AI 输出的几百行代码，连续一个月你也会开始无脑 Accept All。
但数据很残酷：近一半的 AI 生成代码无法通过基础安全测试。更可怕的是，更新更大的模型并没有生成更安全的代码。
有意思的是，Karpathy 自己后来也承认了：当他做自己真正在乎的项目时，他选择了手写代码。vibe coding 的发明者都不 vibe 自己的重要项目。
Heartbleed 的教训
还记得 Heartbleed 吗？OpenSSL 里一个人写的一个 bug，在两年的代码审查中没被发现，暴露了数百万用户的私密通信，修复成本数亿美元。
那只是一个人写的一个 bug。
现在 AI 正在以千倍速度生成代码，覆盖软件栈的每一层。而我们用来防御的手段——代码审查、测试、人工检查——跟漏掉 Heartbleed 两年的是同一套。
更深层的威胁是：当 AI 写代码时，攻击面也变了。如果有人能污染训练数据或入侵模型 API，就能在 AI 生成的每一个系统中植入漏洞。这不是科幻，供应链攻击已经是网络安全中破坏性最大的攻击类型之一。
答案在数学里
Leo de Moura 的观点很直接：我们需要形式化验证。
简单说，就是用数学证明来验证代码是否正确，而不是靠人眼看或跑几个测试用例。你先定义一个「什么是正确」的规范，然后用定理证明器自动检查代码是否满足这个规范。
这听起来很学术，但其实已经有了实际应用：
- CompCert：经过形式化验证的 C 编译器
- seL4：经过形式化验证的操作系统微内核
- s2n-tls：AWS 的 TLS 实现，关键部分有形式化证明
关键点在于：形式化规范独立于生成代码的 AI。当出了问题，你能精确知道是哪个假设失败了。审计人员也能检查。这是测试做不到的——测试只能证明你测过的路径没问题，形式化验证能证明所有路径都没问题。
为什么现在
根据 2022 年的数据，软件质量问题每年给美国经济造成 2.41 万亿美元 的损失。这个数字是在 AI 开始大规模写代码之前统计的。
LLVM 和 Clang 的创造者 Chris Lattner 说得很直白：AI 会同时放大好的和坏的代码结构。好代码在 AI 速度下变得更好，坏代码在 AI 速度下变成「无法理解的噩梦」。
当 AI 开始写金融系统、医疗设备、国防系统、交通控制的代码时，未经验证的代码就不只是质量问题了——它是系统性风险。
写到这里我想到一个讽刺的画面：我们用 AI 以前所未有的速度写代码，然后还得用另一套数学工具来证明这些代码没有搞砸。效率提升了吗？也许。但验证的成本不会消失，只是从写代码的人转移到了验证代码的系统。
不过话说回来，如果连 vibe coding 的发明者都不信任自己 vibe 出来的代码，也许我们确实该认真想想这个问题了。