这期有点特殊，先把话说在前头：不是 repo。arXiv:2610.30188，主分类 cs.SE，顺手把 cs.AI、cs.LG、cs.LO、cs.PL 四个都挂了，五个作者 Zhe Ye、Udaya Ghai、Zhizhen Qin、Dawn Song、Soonho Kong，10 月 20 号挂上去的预印本。
翻 arXiv 翻到它的时候，我第一反应是这玩意儿该怎么报幕——星探的老规矩是甩一个 owner/repo 让你直接去搜，这期没有 star 可看，也没 issue 区可蹲。但这是我最近翻到最像“下一步该长什么样”的东西，也是少见的没法贴一行安装命令的主角。后面解释为什么。
一句话说清楚是什么：让 agent 把代码改快，每改一处，附一份机器能验的等价性证明。不是“测试跑过了”，是“证出来了”。
先说这事为什么值得看。现在这批 coding agent 做性能优化，路径已经很固定：换算法，换数据结构，把递归展开成迭代，把循环拆了，跑一遍测试，绿了就交差。问题在于测试是个代理指标，而 agent 恰好是最擅长对着代理指标做优化的东西。论文直接把这一层点破：已有工作表明 agent 会钻测试的空子，在行为实际上已经变了的前提下把测试糊过去。你让它优化，它给你优化出一个“测试通过”的版本——这两件事从来就不是一回事。
这点我自己有体感。手搓 agent 跑重构，最怕的从来不是它改错，是它改得看起来对。覆盖不到的分支它悄悄动一下，CI 照样一片绿。所以“拿测试验等价”这个默认做法，到了 agent 手上已经不怎么成立。不是测试变差，是优化器的强度变了。
论文的解法很干脆：既然测试不可信，那就要求证明。agent 给出更快的实现，同时产出一份能在 Lean 4 里被机器检验的等价性证明，说明新的和原来的行为一致。Lean 4 是少数几个既能执行程序、又能对程序做推理的家伙，所以任务被形式化成了函数级和代码库级两层。
真正让我坐直的是这一手：它把既有实现本身当规格。
形式化这条路走了几十年，卡脖子的地方从来不是证明器不够强，是没人愿意写规格。你让一个团队先把现有模块的行为形式化描述一遍再谈验证，这话基本谈不动。这篇取巧的地方在于——原来的实现就是规格。你不用描述“这个函数应该干什么”，只要证明“新写的这个对任何输入都和原来那个干同样的事”。规格撰写那道瓶颈，绕过去了。
这一手我服。
绕开的账全记在后头。
Lean 里现成的应用少得可怜，这是硬约束。你不可能要求大家先把 C++ 服务重写成 Lean 再谈优化，那是本末倒置。所以作者写了 Aqueduct，专门干把 C、C++、Go、Rust 的程序迁成原生 Lean 代码这件事，每个迁移结果都要拿回原程序做差分测试，确认移植本身没走样。
这段是全篇最脏最累的活，也是最容易被摘要页那句“验证优化”一笔带过的部分。真正卡住这条路能不能铺开的，是这条迁移流水线的成本和可靠性，不是证明写得多漂亮。17 个完成迁移的应用——这个数字本身就在提醒你现阶段的量级：样板间，不是楼盘。
读到这儿我顺手去翻了翻它引的那几篇讲 agent 钻测试空子的工作，翻完更觉得这个方向是对的。刷着刷着跑题了，拉回来报数字。
先声明，全是作者报的，我一个没复现，这篇我连跑都没法跑。Verina 基准 189 个参考实现，agent 给其中 156 个交出了带证明的更快重写，里面有把指数级递归改成动态规划这种量级的改动——不是常数优化，是真换了做法。那 17 个迁移过来的应用上一共产出 92 个带证明的重写，51 个应用场景里 47 个拿到了加速。
看到 156/189，我第一反应是“这基准是不是太干净了”。函数级、输入输出清楚、依赖不多——这种题面天然适合形式化，也天然不像你手里那个跑着十几个后台任务的仓库。这个怀疑我没法证伪，只能挂着。
然后是我最欣赏这篇的地方：它自己把这种怀疑往下推了一层。作者观察到应用层面的收益明显小于函数层面，于是“该挑哪个函数去优化”本身变成了一个新问题。这话写在正文里是要点胆子的，等于承认函数级那批漂亮数字没法平滑地平移过去。可这也恰恰是它可信的地方——报喜的论文我见得太多了，肯在正文里标出自己这套方法上限在哪的，少。
适合谁：在做 agent 和形式化验证交叉的，直接读，那个“用现成实现当规格”的设定值得抄；做程序合成、超优化、编译器那块、一直想给自动重写加一道可信闸门的，这篇给了一个能落地的形状；还有一类，给 coding agent 做产品、天天被人追问“你怎么保证它没改坏”的——这是我目前见到最正面回答这个问题的一份材料。
不适合谁：想给自家后端提个两成性能的团队，别看了，现阶段这条路走不通。把 C++ 迁到 Lean 的开销，比你自己手动抠三个热点函数高一个数量级，17 个应用的样本量也撑不起任何工程决策。另外对 Lean 4 完全没概念、也不打算学的，读起来会很痛苦——不是它写得晦涩，是这套东西的前提你接受不了的话，后面全是空的。
上手门槛这块，老实讲，没有门槛可言，因为它还没给你能上手的东西。Aqueduct 目前是论文里的一个框架，不是你能 clone 下来的仓库。真要自己验点什么，第一步是把 Lean 4 环境搭起来，那不是十分钟的活。这点我有点遗憾——按老规矩我总想贴一行命令证明门槛低，这期贴不出来。
Aqueduct 进我候选池了。它哪天真放出来，我回来对一遍这篇里的说法，看那几个数还站不站得住。能不能打，等有东西能拉下来那天，你自己跑一圈最准。这期先挖到这儿。