Vero: Can AI Agents Build Formally Verified Software Repositories?
Vero基准评估AI在多模块仓库中联合实现与验证能力，43个实例中最强模型仅解决27个。
核心发现
方法论
Vero采用多阶段手工策划与自动化翻译相结合的策略，将真实软件仓库转化为多模块Lean 4项目，涵盖Python、Dafny、Verus和Coq等语言。每个实例包括API定义、形式规格和参考实现，支持证明和代码+证明两种任务模式。评估采用前沿大模型（如GPT-5.5、Claude）在工具链支持下的联合实现与验证能力，结合正式审计机制检测潜在错误。通过多轮人机协作，确保基准的高质量和多样性，推动仓库级形式验证技术的发展。
关键结果
- 在43个实例中，最强模型在代码+证明模式下仅完全解决27个，且未能解决最难仓库中的任何规格，显示当前AI在大规模仓库级验证任务中仍有明显差距。
- 模型在跨模块不变式、协议一致性和复杂数学理论方面表现较弱，主要原因是缺乏可重用的引理库和全局推理能力，导致部分实现与证明不协调。
- 引入正式审计机制后，发现多个潜在的规格和实现错误，通过形式反例和不满足性证明，显著提升了基准的可靠性和可用性，为未来模型改进提供了明确方向。
研究意义
本研究首次系统性评估AI在仓库级软件验证中的能力，突破了以往只关注单函数或单个证明的局限，提出了多模块、多语言、多任务的联合实现与验证框架。其意义在于推动自动化软件验证从单元级向系统级迈进，为工业界提供更可信赖的自动化工具，解决软件安全性和可靠性中的核心难题。Vero的设计理念和评估结果为未来大规模、全自动化的形式验证提供了宝贵的基准和技术路线，具有深远的学术和工业应用价值。
技术贡献
Vero在技术上创新性地结合了多语言多模块的形式验证场景，设计了支持联合实现与验证的任务架构，提出了基于Lean 4的仓库级验证基准。引入正式审计机制，利用不满足性和反例证明，自动检测潜在的规格和实现错误，增强了基准的鲁棒性。通过多轮人机协作的策划与验证流程，确保了实例的高质量和多样性，为大规模自动化验证提供了可扩展的框架。实验中，评估了当前最先进的代码生成模型（如GPT-5.5、Claude）在复杂仓库中的表现，揭示了模型在跨模块推理和全局一致性方面的不足，为未来算法设计提供了指导。
新颖性
这是首个在仓库级别系统性评估AI联合实现与验证能力的基准，突破了以往只关注单函数或单证明的局限。Vero创新性地支持多语言、多模块、多任务场景，结合正式审计机制，提升了基准的真实性和可靠性。其在任务设计、数据策划和错误检测方面的创新，为推动大规模自动化软件验证提供了新思路，填补了学术界和工业界在此领域的空白。
局限性
- 当前模型在跨模块不变式和协议一致性方面表现不足，缺乏有效的引理库和全局推理能力，导致部分实现与证明不协调，限制了整体性能提升。
- 基准实例规模虽大，但仍受限于Lean 4的表达能力和验证工具的成熟度，未来需要引入更丰富的数学库和优化的验证策略。
- 模型训练数据可能存在偏差，部分实例的结构和规格与训练集高度相似，存在一定的过拟合风险，影响泛化能力。
- 正式审计机制虽有效，但在大规模实例中仍需优化效率，未来需结合更高效的自动化验证工具和推理引擎。
未来方向
未来将致力于提升模型的跨模块推理能力，丰富引理库和数学理论支持，增强全局一致性验证能力。同时，计划扩展到更多源语言和验证场景，结合强化学习和自监督技术，提升模型的自主学习和推理能力。此外，将持续优化正式审计机制，结合更高效的自动化工具，推动仓库级验证的工业化应用，最终实现全自动、可信赖的AI软件生成体系。
AI 总览摘要
在软件工程领域，确保代码的正确性一直是核心挑战。传统的验证方法依赖手工证明和单元测试，既费时又容易遗漏边界条件。随着AI在代码生成中的应用日益普及，如何保证AI生成代码的可信度成为亟待解决的问题。现有的验证基准多局限于单个函数或特定证明任务，难以反映实际软件系统的复杂性。为此，Zhe Ye等人提出了Vero，一个面向仓库级软件验证的基准框架，旨在评估AI在多模块、多语言、多任务环境中的联合实现与验证能力。
Vero的核心创新在于其多阶段策划与自动化翻译流程，将真实软件仓库转化为多模块Lean 4项目，涵盖Python、Dafny、Verus和Coq等多种源语言。每个实例包括API定义、形式规格和参考实现，支持证明和代码+证明两种任务模式。通过人机协作的策划流程，确保实例的高质量、多样性和真实性。特别引入正式审计机制，利用不满足性和反例证明，自动检测潜在的规格和实现错误，显著提升基准的可靠性。
在评估阶段，作者使用最前沿的大模型（如GPT-5.5、Claude）在工具链支持下进行联合实现与验证。结果显示，最强模型在43个实例中仅完全解决27个，且未能解决最难仓库中的任何规格，揭示了当前AI在仓库级验证中的巨大挑战。这些难点主要集中在跨模块不变式、协议一致性和复杂数学理论的验证上，反映出模型在全局推理和引理复用方面的不足。
Vero的研究不仅提供了一个系统性评估平台，也为未来自动化软件验证指明了方向。通过持续优化模型能力、丰富验证工具和引理库，未来有望实现全自动、可信赖的仓库级软件生成，极大推动软件安全和可靠性的发展。尽管目前仍存在性能和效率的限制，但这项工作为学术界和工业界提供了宝贵的基准和技术路线，预示着自动化形式验证的光明前景。
深度解读
原文摘要
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.
参考文献 (20)
LeanAgent: Lifelong Learning for Formal Theorem Proving
Adarsh Kumarappan, Mo Tiwari, Peiyang Song 等
SWE-bench: Can Language Models Resolve Real-World GitHub Issues?
Carlos E. Jimenez, John Yang, Alexander Wettig 等
Program Synthesis with Large Language Models
Jacob Austin, Augustus Odena, Maxwell Nye 等
DafnyBench: A Benchmark for Formal Software Verification
Chloe Loughridge, Qinyi Sun, Seth Ahrenbach 等
Evaluating Large Language Models Trained on Code
Mark Chen, Jerry Tworek, Heewoo Jun 等
LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code
Naman Jain, King Han, Alex Gu 等
This Paper Is Included in the Proceedings of the 12th Usenix Symposium on Operating Systems Design and Implementation (osdi '16). Certikos: an Extensible Architecture for Building Certified Concurrent Os Kernels Certikos: an Extensible Architecture for Building Certified Concurrent Os Kernels
Ronghui Gu, Zhong Shao, Hao Chen 等
VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
Yutong Xin, Qiaochu Chen, Greg Durrett 等
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu 等
A benchmark for vericoding: formally verified program synthesis
Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin 等
Clover: Closed-Loop Verifiable Code Generation
Chuyue Sun, Ying Sheng, Oded Padon 等
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises
Andres Erbsen, Jade Philipoom, Jason Gross 等
Certified Program Synthesis with a Multi-Modal Verifier
Yue Feng, Dipesh Kafle, V. Gladshtein 等
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
Kyle Thompson, Nuno Saavedra, Pedro Carrott 等
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
Haoyu Zhao, Ziran Yang, Jiawei Li 等
The Coq proof assistant : reference manual, version 6.1
Bruno Barras, S. Boutin, C. Cornes 等
miniCodeProps: a Minimal Benchmark for Proving Code Properties
Evan Lohn, S. Welleck
The Lean Theorem Prover (System Description)
L. D. Moura, Soonho Kong, J. Avigad 等
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel 等