前几天后半夜值班，pager 难得安静。闲着也是闲着，我干了件更丧的事：刷 arXiv。
cs.SE 分类底下，8 月 30 号挂出来一篇，一帮人用 VST 给 liblzma 的解码部分做了内存安全验证。liblzma 就是 xz-utils 里那个压缩库，你解过的每一个 .tar.xz，过的都是它的手。
这种标题我平时直接划走，「形式化验证」四个字在我们的世界里约等于别人家的玩具。这次停下来了，因为摘要里提了一句：证明脚本是 AI agent 辅助写的。
我心想，又来了。AI 写证明？把幻觉换个格式输出罢了。
结果看完分工，我把这句咽回去了。
他们的排法是：agent 生成证明目标、提优化；人写规范、审模型，语义上的改动必须人点头；最后，Rocq 的内核检查每一个证明项。
注意最后这条。不是“人审一眼 agent 的输出”，是内核检查。内核这东西不睡觉，不赶 deadline，也不吃“看起来对”这一套，证明项里有一个符号对不上，它就拒收。agent 可以幻觉出十万行证明，拒收就是拒收。
这是我这两三年见到的第一个不让我本能反胃的 AI 分工。
因为这次，拍板的不是人。我平时的世界是这样的：agent 生成一个变更，diff 挺像回事，凌晨三点一个困得眼花的人点了 approve。裁判是人，人会累，会被说服，会想赶紧回去睡。这个剧本，我接过的电话里一半是它。
而那边，裁判是个物理上没法放水的程序。
代价呢？论文贴得很老实。整个活拆成 27 个证明，最大那个对着 lzma_decode：
lzma_decode: 338 行 C（预处理后 1934 行）
证明脚本: 183268 行
机器提取的目标语句: 775768 行
会有人拿这个笑他们。二十万行证明，换三百多行代码？我第一眼也笑了。
第二眼笑不出来。想想我们这边一天让 agent 往 MR 里喷几千行、审的人平均每行停留两秒的场面，人家是给“确定”标了价格，我们是给“快”标了个零，账全记在半夜接电话的冤种头上。
「AI 提效十倍」的那个十倍里，从来不含验证成本。因为压根没验证。
再说这论文顺带挖出来的东西。验证过程中发现 LZMA1 处理空输入的路径上有货真价实的未定义行为：range decoder 的宏对空指针做了加零，还做了两个空指针的相减。C 标准白纸黑字，这俩都是 UB。
天天在你我机器上解压缩的库，里面埋着教科书级的 UB 🙃 至于实际跑起来为什么没出事，那是另一回事。UB 的意思从来不是“会崩”，是“有没有事全看编译器心情”。哪天升个版本、开个优化，它有合法的权力让你崩，而且崩的时候你连该找谁都找不到。
我这职业生涯见过太多这种“一直没事”的 UB，这段看得有点脊背发凉。祖传代码就这样——你不知道哪一行丑的是雷管，这篇等于拿着探雷器给你标出来一块。
补一刀：作者们还算老实。论文里明说重点不是生成新的已验证代码，是对现有的生产级 C 做验证；也交代了最难的活不是写证明，是把生产 C 翻译建模、搭驱动 Rocq 的框架、给