UC Berkeley 等机构发布 Vero，据称是首个要求智能体在仓库级同时编写实现与证明的基准，含 43 个多模块 Lean 4 实例、743 个计分 API 和 2705 条形式化规范。
AI 编码代理现在可以在整个代码库中进行修改。但在代理输出“所有测试通过”之后，我们能否信任它们以及它们的代码？
AI 编码代理现在可以在整个代码库中进行修改，并且通常会以报告“所有测试通过”作为结尾。这个报告的价值没有听起来那么高，因为测试只检查某人写下的案例。形式化验证提供了更强的保证。它会生成机器检查的证明，证明实现满足其规范中的每个输入，而不仅仅是测试套件中的输入。所以，自然的问题是，AI 代理是否能够在真实代码库中达到这一标准。它能否在多模块代码库中实现每个所需的 API，证明每个提供的规范，并在整个过程中保持代码、证明和构建的一致性？我们创建了 Vero 来准确地衡量这一点。
据我们所知，Vero 是第一个要求代理在代码库级别同时编写实现和证明的基准。它包含 43 个多模块的 Lean 4 实例，这些实例经过精心挑选，来自原本用 Python、Dafny、Verus 和 Coq 编写的真实项目。在整个测试套件中，代理面临 743 个评分的 API 和 2,705 个形式化规范。
该基准以两种模式运行。在仅证明模式下，代理接收参考实现并针对其证明规范。在代码与证明模式下，代理自己编写每个所需的 API，然后证明自己的代码满足每个规范。
我们评估的最强配置是 GPT-5.5（xhigh）与 Codex 组合，在代码与证明模式下完全解决了 43 个实例中的 27 个，在仅证明模式下解决了 43 个实例中的 25 个。分别通过了 87.3% 和 85.8% 的单个规范。即便如此，每种配置在两种模式下仍有 10 个实例未解决。综合来看，这些数据表明，证明单个规范已经不再是难点。难点是保持整个证明代码库的一致性，使所有内容都能构建并完成每个义务。
完整的仓库完成比按规范成功要困难得多。GPT-5.5（xhigh）在 code-and-proof 中通过了 87.3% 的规范，在 proof-only 中通过了 85.8%，但完全完成的实例仅为 27/43 和 25/43。Vero 仅在每个提供的规范均被证明且评分仓库仍可构建且无公理错误时，才将一次运行计为完整解决。
可重用引理库在完整解决中是一种一致的模式。在 82 次完整解决运行中，代理编写的辅助定理在 code-and-proof 中包含证明行的中位数为 73.6%，在 proof-only 中为 71.6%。在 82 次完整解决中，有 80 次至少有一个辅助定理支持两个或更多规范；有 65 次辅助定理支持至少五个规范。
实现自由既有帮助也有阻碍。代理有时会用一个满足相同规范的更简单实现来替代难以证明的参考算法。论文识别出三份仓库中有五个实例-代理对这种情况下获得帮助。相反，17 对匹配实例在 proof-only 中是完整解决，但在 code-and-proof 中不是。
该基准仍有很大提升空间。在两种模式下，每种配置均未解决的实例有 43 个中的 10 个。论文将许多残余失败与全局不变量、重复行为、提供的定义以及可重用引理的深层链条联系起来。
大多数已验证代码的基准测试关注单个函数。那少数的仓库级基准通常提供固定实现，并仅评估证明生成。因此，它们忽略了真实验证工作中的一个核心难点：实现和证明的选择会在整个代码库中相互影响。
Vero 将这种耦合转化为任务。代理必须在多模块 Lean 4 项目中做出一致选择，而不仅仅是解决一系列独立的证明空洞。这揭示了长程证明工程、实现-证明协调以及构建维护，而函数级评估无法衡量这些。
每个 Vero 实例都是一个独立的 Lean 4 项目。Lean 4 是一种编程语言和定理证明器，其中证明由一个小型可信内核进行检查。策展人提供三个冻结内容层：
共享数据类型和帮助器定义。
定义必须实现的 API 签名。
以谓词形式编写的形式化规范，作用于整个仓库范围的实现接口。
代理填写实现主体和证明义务。完整解决方案要求每个指定义务在评分器从干净的基准源重建仓库时均能通过。
图1. Vero 的端到端构建、评估、评分和形式审计工作流程。
仅证明模式。基准提供参考实现。代理必须针对其证明每个规范。这在保留仓库级依赖的同时隔离了证明构建。
代码与证明模式。参考实现主体被保留。代理编写每个所需的 API 主体，并针对自己的实现证明每个相应的规范。这是 Vero 的主要联合生成设置。
代码与证明模式增加了超出任务堆叠的实现义务。一个易于证明的算法可能比一个忠实但难以实现的参考算法更容易验证，而不良的实现选择可能产生新的证明义务或破坏构建。
评分器仅从允许的代理可编辑区域提取内容，将其插入从基准源渲染的新项目中，并重建完整项目。它根据公理允许列表检查证明依赖关系，并使用基于规则和大型语言模型评判的筛选来拒绝使义务变得微不足道的声明或类型类实例。这些安全措施旨在确保被认可的证明经过机器检查，并且不依赖于对冻结基准内容的编辑或不允许的公理。
Vero 包含 43 个实例：13 个从使用 Dafny、Verus 或 Coq 编写的支持验证的项目翻译而来，30 个从 Python 项目翻译而来，策展人还为这些项目编写了形式化规范。该套件涵盖智能合约和区块链协议、分布式系统与共识、安全关键基础设施、形式数学、数据结构、算法和数值工具。
策展流程遵循发现、选择、计划、翻译、必要时编写规范和验证。每个阶段都作为大型语言模型（LLM）代理在人工审核门后运行。最终生成的 Lean 4 实现、规范和真实证明是新型策展工作；在被评估的实例中，没有可用的预先存在的公共 Lean 4 真实数据。
评估涵盖两种代理平台下的四种前沿编码代理配置。每次运行都能完全访问文件系统、构建工具和 Lean 工具链，并有 90 分钟的实际时间预算。
表 1. 90 分钟预算后的完整仓库结果。
GPT-5.5（xhigh）在 45 分钟内完成 25 个代码与证明的完整解决方案以及 23 个仅证明的完整解决方案。即便如此，大多数已解决的实例仅被一个配置完成，且八种代理模式组合中仍有 10 个实例未解决。
图 2. 完整解决轨迹与精确完整解决矩阵。
Vero 将完整解决作为主要结果，因为部分规范覆盖可能因较易的任务而被夸大。在代码与证明模式下，一个未证明的规范可能表示缺少证明或实现未通过该规范。每个规范的覆盖情况仍具有诊断意义，但只有完整覆盖才能保证提交的实现符合所有基准规范。
在 82 次完整解决运行中，辅助定理占代码与证明模式下证明行数的中位数为 73.6%，在仅证明模式下为 71.6%。一个辅助定理在 82 次完整解决中至少支持两个规范的次数为 80 次，至少支持五个规范的次数为 65 次。
助手链深度与其他运行的低通过率相关。在无辅助定理的情况下，代码与证明模式下的规范通过率为 83.9%，仅证明模式下为 80.1%。当链深度达到 4 或更高时，通过率降至 50.6% 和 39.1%。这一模式表明需要更好的不变量发现、证明依赖规划和可重用的本地库。
图 3. 证明助手重用、证明行占比及助手链通过率。
我们的论文在三个代码库中识别了5个实例-代理对，其中代理将硬引用算法替换为满足相同规格的更简单实现。通过修改这5个对，代码与证明方法完成了所有250条规格，而仅证明方法在固定参考实现上完成了201条。实现的收益主要在于可证明性，而不一定是生产质量。一些替代方案牺牲了渐近效率。
自由度也可能增加难度。17个匹配的实例-代理对在仅证明方法中可以完全解决，但在代码与证明方法中不行。轨迹分析显示，代理倾向于早期确定一个实现并持续扩展证明直到截止日期，而不是在证明计划反复停滞时重新审视定义。
形式化验证基准仍可能包含在类型检查、成功构建和策展人审核中幸存的潜在错误。Vero将这些错误转化为迭代质量改进循环：它的审计机制接受三种形式的机器检查负面证据，而不是将不可能的证明义务视为代理失败：
参考实现违反了规范。
没有实现能够满足某个单独规格。
一组规格在单独可满足的情况下整体不一致。
每个形式化见证将受影响的实例返回给策展人审核，并帮助指导修正。每个确认的缺陷在报告的评估前都已修复。同样的反馈循环使未来代理在能力提升并发现更微妙问题时能够持续改进基准。
代码库规模的经过验证代码生成提供了比仅测试更强形式保证的试验场，尤其适用于高保障软件。结果表明，当前代理可以通过构建大量证明库、识别基准缺陷，有时优化现有算法以增强可证明性，完成这些任务的有意义部分。剩余的差距在于代码库规模的组织：发现共享不变式、协调代码与证明，并保持整个工件的一致性和可构建性。
推动去中心化和人工智能的科学、技术与教育，以赋能负责任的数字经济。
AI coding agents can now make changes across entire repositories. But after an agent outputs “all tests pass,” can we trust them and their code?
AI coding agents can now make changes across entire repositories, and they usually finish by reporting that all tests pass. That report is worth less than it sounds, because tests only check the cases someone thought to write down. Formal verification gives a much stronger guarantee. It produces a machine-checked proof that an implementation satisfies its specification on every input the specification covers, not just the ones in a test suite. So the natural question is whether an AI agent can actually work at this standard across a real codebase. Can it implement every required API in a multi-module repository, prove every supplied specification, and keep the code, the proofs, and the build consistent the whole way through? We built Vero to measure exactly that.
Vero is, to our knowledge, the first benchmark that asks agents to write implementations and proofs together at the repository level. It contains 43 multi-module Lean 4 instances curated from real-world projects originally written in Python, Dafny, Verus, and Coq. Across the suite, agents face 743 scored APIs and 2,705 formal specifications.
The benchmark runs in two modes. In proof-only mode, the agent receives reference implementations and proves the specifications against them. In code-and-proof mode, the agent writes every required API itself and then proves that its own code satisfies every specification.
The strongest configuration we evaluated, GPT-5.5 (xhigh) with Codex, fully solves 27 of 43 instances in code-and-proof mode and 25 of 43 in proof-only. It passes 87.3% and 85.8% of individual specifications, respectively. Even so, 10 instances remain unsolved by every configuration in both modes. Taken together, the numbers show that proving individual specifications is no longer the hard part. The hard part is holding an entire proof repository together so that everything builds and every obligation closes.
Repository completion is much harder than per-specification success. GPT-5.5 (xhigh) passes 87.3% of specifications in code-and-proof and 85.8% in proof-only, but fully completes only 27/43 and 25/43 instances. Vero counts a run as a full solve only when every supplied specification is proved and the graded repository remains buildable and axiom-clean.
Reusable lemma libraries are a consistent pattern in full solves. Across 82 full-solve runs, agent-written helper theorems contain a median of 73.6% of proof lines in code-and-proof and 71.6% in proof-only. In 80 of 82 full solves, at least one helper supports two or more specifications; in 65, a helper supports at least five.
Implementation freedom helps and hurts. Agents sometimes replace a hard-to-prove reference algorithm with a simpler implementation satisfying the same specifications. The paper identifies five instance-agent pairs across three repositories where this helps. Conversely, 17 matched pairs are full solves in proof-only but not code-and-proof.
The benchmark has substantial headroom. 10 of 43 instances remain unsolved by every configuration across both modes. The paper links many residual failures to global invariants, repeated behavior, supplied definitions, and deep chains of reusable lemmas.
Most verified-code benchmarks focus on individual functions. The few repository-scale benchmarks generally provide a fixed implementation and evaluate proof generation alone. They therefore omit a central difficulty of real verification work: implementation and proof choices affect each other across a codebase.
Vero turns that coupling into the task. Agents must make coherent choices across a multi-module Lean 4 project, not solve a sequence of independent proof holes. This exposes long-horizon proof engineering, implementation-proof coordination, and build preservation that function-level evaluations do not measure.
Each Vero instance is a self-contained Lean 4 project. Lean 4 is a programming language and theorem prover in which proofs are checked by a small trusted kernel. The curator supplies three frozen content layers:
Shared data types and helper definitions.
API signatures defining what must be implemented.
Formal specifications written as predicates over a repository-wide implementation interface.
The agent fills implementation bodies and proof obligations. A full solve requires every specified obligation to pass when the grader rebuilds the repository from a clean benchmark source.
Figure 1. Vero’s end-to-end construction, evaluation, grading, and formal-audit workflow.
Proof-only mode. The benchmark supplies the reference implementation. The agent must prove every specification against it. This isolates proof construction while retaining repository-scale dependencies.
Code-and-proof mode. Reference implementation bodies are withheld. The agent writes every required API body and proves each corresponding specification against its own implementation. This is Vero’s primary joint-generation setting.
Code-and-proof adds implementation obligations beyond task stacking. A proof-friendly algorithm may be much easier to verify than a faithful but difficult reference algorithm, while a poor implementation choice can create new proof obligations or break the build.
The grader extracts content only from permitted agent-editable regions, inserts it into a fresh project rendered from the benchmark source, and rebuilds the full project. It checks proof dependencies against an axiom allowlist and uses rule-based and LLM-judge screens to reject declarations or typeclass instances that trivialize obligations. These safeguards are designed to ensure that credited proofs are machine-checked and do not depend on edits to frozen benchmark content or disallowed axioms.
Vero contains 43 instances: 13 translated from verification-aware projects written in Dafny, Verus, or Coq, and 30 translated from Python projects for which the curators also write formal specifications. The suite spans smart contracts and blockchain protocols, distributed systems and consensus, security-critical infrastructure, formal mathematics, data structures, algorithms, and numerical utilities.
The curation pipeline follows discover, select, plan, translate, specification writing when needed, and validate. Each stage runs as an LLM agent behind a human-review gate. The resulting Lean 4 implementations, specifications, and ground-truth proofs are novel curation work; no pre-existing public Lean 4 ground truth was available for the evaluated instances.
The evaluation covers four frontier coding-agent configurations under two agent harnesses. Every run receives full file-system, build, and Lean toolchain access and a 90-minute wall-clock budget.
Table 1. Full-repository outcomes after the 90-minute budget.
GPT-5.5 (xhigh) reaches 25 code-and-proof and 23 proof-only full solves within 45 minutes. Even so, most solved instances are completed by only one configuration, and 10 instances remain unsolved across all eight agent-mode combinations.
Figure 2. Full-solve trajectories and exact full-solve matrix.
Vero uses full solve as the primary outcome because partial specification coverage can be inflated by easier obligations. In code-and-proof mode, an unproved specification can indicate either a missing proof or an implementation that does not pass the specification. Per-specification coverage remains useful diagnostically, but only complete coverage certifies the submitted implementation against all benchmark specifications.
Across the 82 full-solve runs, helper theorems contain a median of 73.6% of proof lines in code-and-proof and 71.6% in proof-only. One helper supports at least two specifications in 80 of 82 full solves and at least five in 65.
Helper-chain depth is associated with lower pass rates in other runs. Specifications with no helper pass at 83.9% in code-and-proof and 80.1% in proof-only. At a chain depth of 4 or more, the pass rates fall to 50.6% and 39.1%. The pattern points to a need for better invariant discovery, proof-dependency planning, and reusable local libraries.
Figure 3. Proof-helper reuse, proof-line share, and helper-chain pass rates.
Our paper identifies 5 instance-agent pairs across 3 repositories where an agent replaces a hard reference algorithm with a simpler implementation satisfying the same specifications. Via modifying those 5 pairs, code-and-proof closes all 250 specifications, while proof-only runs against the fixed reference close 201. The gain of implementation is mainly provability, and not necessarily production quality. Some substitutions sacrifice asymptotic efficiency.
Freedom can also add difficulty. 17 matched instance-agent pairs are full solves in proof-only but not code-and-proof. The trajectory analysis shows agents tend to commit to an implementation early and keep growing proofs until the deadline, rather than revisiting a definition when a proof plan repeatedly stalls.
Formal-verification benchmarks can still contain latent errors that survive type-checking, successful builds, and curator review. Vero turns those errors into an iterative quality-improvement loop: rather than treating an impossible proof obligation as an agent failure, its audit mechanism accepts three forms of machine-checked negative evidence:
The reference implementation violates a specification.
No implementation can satisfy an individual specification.
A set of specifications is jointly inconsistent even though its members are individually satisfiable.
Each formal witness sends the affected instance back to curator review and helps guide a correction. Every confirmed defect was repaired before the reported evaluation. The same feedback loop enables continuous benchmark improvement as future agents grow more capable and uncover subtler problems.
Repository-scale verified code generation offers a testbed for a stronger form of assurance than tests alone, particularly for high-assurance required software. The results show that current agents can complete a meaningful fraction of these tasks by building substantial proof libraries, identifying benchmark defects, and sometimes optimizing existing algorithms for provability. The remaining gap is repository-scale organization: discovering shared invariants, coordinating code and proof, and keeping the entire artifact consistent and buildable.
Advancing the science, technology, and education of decentralization and AI to empower a responsible digital economy.
扫码直达文章详情