1. Specification-first convergence with an AI coding agent
- 作者/来源： Joël Abenhaïm / AI Sovereign Labs
- 发布日期： 2026-08-12
- arXiv： https://arxiv.org/abs/2608.12440
- AlphaXiv： https://www.alphaxiv.org/abs/2608.12440
推荐理由： 这篇不是普通的 SWE-bench 实验，而是一份带完整过程证据的大型生产代码库重构案例。它最值得关注的不是“Agent 一次改了多少文件”，而是把 specification-first、冻结目标、反复审计、编译测试反馈、再对冻结 specification 做 verification 串成了一个可收敛的工程流程。对 software factory 来说，这比单纯增加 Agent 自主性更有启发：先把“什么算完成”变成稳定、可审计的中间表示，再让 Agent 围绕它持续纠偏。
核心要点：
- 目标代码库是约 71.8 万行 TypeScript、3,648 个文件。任务是拆除一个核心生命周期 invariant，让流式 AI 请求在 UI panel 被关闭后仍持续，并在重新打开时无丢失、无重复地重新挂接；最终修改涉及 189 个文件。
- 流程先由 Agent 形成 formal specification，随后进行了 14 轮 specification refinement；实现后又进行了 17 轮代码对冻结 specification 的 verification。31 次审计共发现并修正 201 个问题，收敛条件是连续两轮 verification 零发现。
- 整个重构耗时约 3 天、成本 2,430 美元。但这是单一案例，不能直接外推为通用成功率；它更重要的贡献是提供了一种工程范式：specification 作为稳定控制面，Agent 作为可替换执行器，verification loop 负责逼近目标。
2. Vero: Can AI Agents Build Formally Verified Software Repositories?
- 作者/来源： Zhe Ye、Hantao Lou、Yuechun Sun、Peiyang Song、Zhengxu Yan、Timothe Kasriel、Qingyang Zhang、Kaiyu Yang、Soonho Kong、Jingxuan He、Dawn Song
- 发布日期： 2026-08-13
- arXiv： https://arxiv.org/abs/2608.13522
- AlphaXiv： https://www.alphaxiv.org/abs/2608.13522
- 代码/Benchmark： https://github.com/sunblaze-ucb/vero
推荐理由： 当前 coding agent 大多靠 tests 判断“代码能不能工作”，Vero 把要求提高到：Agent 不仅要实现代码，还要生成机器可检查的证明，证明整个多模块 repository 满足 specification。 这很可能是高可靠 AI-native software factory 的重要方向——把 verifier 从辅助工具提升为交付链的一部分。
核心要点：
- Vero 包含 43 个多模块 Lean 4 repository 实例、743 个 API、2,705 条 specification，来源覆盖 Python、Dafny、Verus、Coq 的真实项目，并同时评估 proof-only 和 code-and-proof 两种模式。
- code-and-proof 模式允许 Agent 自己选择实现，因此它可以主动把算法改写成更容易证明的形式；但实现与证明是耦合的，局部重写也可能破坏其他模块的 proof。这比“给定实现再补证明”更接近真实的 verified software engineering。
- 当前 frontier agent 仍有明显缺口：最强配置 GPT-5.5 xhigh + Codex 在 code-and-proof 模式完整解决 27/43 个 repository，最难的 10 个实例没有任何配置完成。主要失败集中在跨模块 invariant、protocol consistency 和需要共享 lemma library 的长链证明上。