VerusWeave：并发 Verus 程序证明修复基准
原标题：VerusWeave: A Benchmark for Proof Repair in Concurrent Verus Programs
AI 摘要
来自 INESC-ID 和里斯本大学的研究者提出了 VerusWeave，这是首个专门针对并发 Verus 程序证明修复的基准，由四个开源项目衍生而来，包含 75 个聚焦任务和 17 个完整模块级变体。任务要求编码智能体在不改动可执行代码和规范的前提下补全证明注解，评测框架使用 Verus 和变更检查器验证修复结果。对四种通用编码智能体框架的初步评测显示，聚焦任务成功率为 75–85%，完整模块变体仅 29–47%，表明模块级自主证明修复仍具挑战。
正文节选
[Page 1] VerusWeave: A Benchmark for Proof Repair in Concurrent Verus Programs Pedro Ribeiro∗, Martim Afonso∗, André Vasconcelos∗, João F. Ferreira† ∗INESC-ID and Instituto Superior Técnico, Universidade de Lisboa, Portugal †INESC-ID and Faculty of Engineering, University of Porto, Portugal Abstract—Concurrent software underpins critical infrastruc- requires reasoning about inter-thread interfere