发表机构
University of Chicago; California Institute of Technology; Stanford University; UC Berkeley; Amazon Web Services; Apodex（芝加哥大学; 加州理工学院; 斯坦福大学; 加州大学伯克利分校; 亚马逊云计算服务; Apodex）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究推出首个仓库级验证软件综合基准Vero，含43个多模块实例，评估发现前沿智能体仅解决27个实例，为相关研究提供测试平台。
AI 中文摘要
AI智能体正越来越多地被用于编程，但无法为生成代码的正确性提供任何保证。验证式代码生成（即智能体同时生成实现代码及其规范的机器可检验证明）为实现可信的AI生成软件提供了更可靠的途径。该方向现有的基准要么聚焦于单个函数，要么仅基于已提供的实现评估证明生成。智能体能否在真实的多模块代码库中做出一致的实现与证明选择，仍是一个开放问题。为弥合这一差距，我们推出Vero，这是首个用于评估仓库级联合实现与证明综合的基准。Vero包含43个来自真实仓库的多模块实例，涵盖Python、Dafny、Verus和Coq，涉及从密码协议到分布式系统的多样化领域。每个实例均包含一个具有预定API接口、人工整理的形式化规范及参考实现的多模块Lean 4仓库，支持仅证明和代码加证明两种评估模式。为提升基准可靠性，Vero还包含一个审计机制，允许智能体对所提供规范的不可满足性或参考代码的不正确性进行形式化证明，该机制在整理过程中可发现并修正潜在的代码和规范错误。我们结合Lean工具链评估了前沿编码智能体配置，最强的智能体仅完全解决了43个实例中的27个，且在最难的仓库上未闭合任何规范。Vero为衡量仓库级验证软件综合的进展提供了具体测试平台，当前智能体仍存在不足。我们在该httpsURL发布了此基准、整理流程及评估工具。
英文摘要
AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.
