{"id":"85c4621f-7949-4afc-94d7-358ac402123a","arxiv_id":"2608.13522","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Vero is the first repository-level benchmark for joint implementation and proof synthesis in Lean 4, and the best tested agent fully solves only 27 of 43 instances.","lead":"Vero is a new benchmark that tests whether AI coding agents can both implement and formally prove correct multi-module software repositories in Lean 4. Across 43 real-world-derived instances, the strongest agent fully solves only 27, showing that repository-scale verified software synthesis remains out of reach.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central interpretation depends on 2,705 manually curated Lean specifications faithfully capturing upstream behavior; the audit in Section 3.5 certifies formal satisfiability, not semantic correctness, and Appendix F documents 38 latent specification defects that survived manual review.","rationale":"The reader's weakest assumption identifies the same load-bearing concern: benchmark validity depends on the 2,705 manually curated Lean specifications faithfully capturing the intended behavior of the upstream repositories. I agree, and the paper's own evidence strengthens the concern. The audit mechanism can only certify formal satisfiability, not semantic correctness, and Appendix F reports 38 latent specification defects in 9 of 43 released instances, showing that such errors do survive manual review and type-checking. The absence of ground-truth Lean proofs means there is no positive certificate that the reference implementation satisfies all remaining specifications, so some of the unsolved instances could reflect benchmark defects rather than agent capability. The single-run/no-variance issue noted by the reader is real but secondary: cross-configuration consistency in the failure patterns (for example, the same seven-specification residual on verdict across all configurations) suggests the 10-instance result is more robust than a single-run variance objection alone would imply. The appropriate response is therefore to keep the CONDITIONAL verdict and require the spec-fidelity audit as a condition, not to reject the paper.","tokens_in":26744,"tokens_out":8586,"duration_ms":105730,"concrete_test":"Run a dedicated audit pass on the ten instances that no configuration fully solved, using an independent agent configuration whose sole instruction is to produce machine-checked negative certificates for every specification: ¬S(canonical), ¬∃impl, S(impl), or joint inconsistency of a subset. Grade all certificates with the same anti-cheating layers used in Section 4. If any new certificate type-checks, that instance contains a latent specification defect and the 'resists all configurations' finding is partly a benchmark artifact. If, across five independent audit runs per instance, no negative certificate is found, the specification-fidelity concern for the headline result is substantially weakened.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's conclusion that current agents lack repository-scale verification organization holds only if agent failures reflect verification capability rather than benchmark defects. In proof-only mode, a specification that is false of the reference implementation is unsolvable by construction; in code-and-proof mode, an unsatisfiable specification is similarly impossible to solve. The audit mechanism (Section 3.5) can formalize negative evidence such as unsatisfiable or mutually inconsistent specifications, but it cannot detect a satisfiable specification that misstates the intended behavior, and the limitations section (Section 5) explicitly concedes that the audit does not certify semantic correctness. Appendix F makes this risk concrete: across the released instances the audit produced 38 adjudicated specification defects in 9 instances, including a directly contradictory pair on verdict and false length assumptions on verified_bitmasks, all of which survived type-checking and manual review. Because the benchmark deliberately contains no Lean ground-truth proofs (a contamination safeguard), there is no positive certificate that the reference implementation satisfies every remaining specification; the positive certificates mentioned in Appendix F cover only repaired specs. If residual false or unsatisfiable specifications remain, they would inflate both the 10-instance 'resists all configurations' result and the 27-of-43 ceiling, making semantic fidelity the load-bearing assumption for the central claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper introduces Vero, a repository-level benchmark for verified code generation in Lean 4, constructed from 43 instances translated from Dafny, Verus, Coq, and Python repositories, with 743 scored APIs and 2,705 scored specifications. The benchmark supports both proof-only and code-and-proof evaluation modes, includes an anti-cheating grader and a formal audit mechanism that accepts machine-checked negative evidence about specifications, and is evaluated with four frontier coding-agent configurations. The authors report that the strongest configuration fully solves only 27 of 43 instances in code-and-proof mode and 25 in proof-only mode, that 10 instances resist all eight evaluated configurations, and that successful runs depend on building reusable lemma libraries rather than local proof skill.","tokens_in":26941,"tokens_out":7894,"duration_ms":85416,"significance":"If the benchmark specifications are semantically faithful, Vero is a valuable contribution to the verified-code-generation literature: it is the first benchmark, to my knowledge, to require joint implementation and proof synthesis at repository scale, and it does so in a multi-language, multi-domain setting. The paper's strengths include its detailed anti-cheating layers with concrete attack examples, the formal audit mechanism with human-adjudicated case studies, per-instance pass counts in the appendix, and the authors' willingness to manually inspect substitutions and failure artifacts. The main scientific value as evidence about agent verification capability, however, rests on the semantic fidelity of 2,705 manually curated specifications, which is also the point of greatest residual risk.","major_comments":[{"comment":"The paper's central interpretation that the 10 'resists all configurations' instances and the 27-of-43 ceiling reflect a gap in agents' verification capability presupposes that every one of the 2,705 specifications is semantically faithful to the upstream repository and satisfiable by the reference implementation. Appendix F directly documents that this presupposition failed 38 times across 9 instances, including a directly contradictory pair on verdict and false length assumptions on verified_bitmasks, all of which survived type-checking and manual review. Section 5 concedes that the audit certifies formal satisfiability but not semantic correctness, and the benchmark deliberately contains no Lean ground-truth proofs as a contamination safeguard, so there is no positive machine-checked certificate that the remaining specifications hold of the reference implementations. A false or unsatisfiable residual specification would make a proof-only instance unsolvable by construction and a code-and-proof instance nearly so, inflating both the 'resists all configurations' count and the 27/43 ceiling. I request an additional validation artifact: for every instance, a curator-written sanity proof in a branch not exposed to agents that each specification holds of the reference implementation, or, failing that, a quantitative residual-risk analysis reporting how many of the 2,705 specifications were formally audited and with what outcome.","section":"§3.3, §3.5, §5, Appendix F"},{"comment":"The claim that code-and-proof mode measures repository-scale verified software generation is weakened by implementation substitution, which the paper itself documents. In Appendix G, the munkres Hungarian-algorithm reference is replaced by a 164-line permutation enumeration by three agents, and in Appendix H.4 sortedcontainers' O(log n) bisection is replaced by an O(n) linear scan; across five audited pairs the agents close 250 specifications in code-and-proof versus 201 in proof-only. These are behaviorally correct with respect to the scored specifications but are not faithful reconstructions of the upstream repositories, and the missing cost behavior is explicitly a gap in the metric. The paper should separate 'faithful' full solves from 'substituted' full solves in all headline numbers and either add complexity specifications to the benchmark or state clearly that the benchmark deliberately measures specification satisfaction rather than repository reconstruction.","section":"§4.2, Appendix G, Appendix H.4"},{"comment":"All reported full-solve counts are based on a single run of each configuration per instance. LLM-agent outcomes are stochastic, and full solve is a Boolean decision, so the point estimates 27, 25, 8, and 2, and the exact ordering of configurations, may not be stable. The 'frontier-resistant' claim depends on these counts. Please add at least three repeated runs for the strongest configuration on a subset of instances, or a small multi-run study for all configurations, and report the spread; alternatively, explicitly qualify the headline counts as single-sample observations, since the per-instance pass-count table alone does not provide this information.","section":"§4.1, Figure 3, Table 4"}],"minor_comments":[{"comment":"The text credits CoqStoq to reference [29], but the reference list entry [29] is 'Rango: Adaptive retrieval-augmented proving...' by Thompson et al.; please check whether this is the intended citation or add the missing CoqStoq reference.","section":"§2, reference [29]"},{"comment":"The notation overloads S as both a set and a proposition (for example, '∀ S∈S′' and later 'S(impl)' appear in the same formula); using lower-case letters for individual propositions would make the condition clearer.","section":"§3.5, Eq. (3)"},{"comment":"The caption 'Exact full-solve matrix' is not self-explanatory; clarify what the rows and columns represent and what the entries 0×, 1×, 2×, and ≥3× mean.","section":"Figure 3(c) caption"},{"comment":"The proof of the auxiliary conjunction appears to be cut off after 'induction t ...' with empty lines; please include the complete proof or an explicit ellipsis.","section":"Appendix H.1, deposit_sc proof block"},{"comment":"The dedekind_reals rows show 0/82 in every cell; even if the instance is intended as a hard case, the main text should explicitly state whether the audit found any specification defects there, since a uniform 0 across all configurations is exactly the pattern a false or unsatisfiable specification would produce.","section":"Table 4, dedekind_reals rows"}],"recommendation":"major_revision","confidential_remarks":"To the editor: I recommend major revision rather than rejection. The benchmark is valuable, the authors are unusually forthcoming about limitations, and the core methodology is sound. The main risk is semantic fidelity of the specifications, which is load-bearing for the paper's central claim; a supplement with positive sanity certificates or a formal audit coverage report would substantially increase confidence. I do not see grounds for rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This is a real benchmark contribution, not a wrapper around existing tasks. Vero is the first evaluation I know that asks agents to produce both implementations and machine-checked Lean 4 proofs across whole multi-module repositories, rather than individual functions or proof obligations against fixed code. The curation pipeline is serious: 43 instances from Dafny, Verus, Coq, and Python, 2,705 specifications, per-instance provenance with pinned upstream commits, and an audit mechanism that accepts machine-checked negative evidence. That audit is the best part. Appendix F is convincing: contradictory specifications on verdict, unsatisfiable comparator-law gaps on verified_ironkv, missing length preconditions on verified_bitmasks — 38 defects that survived manual review and were caught by the audit. This is exactly the kind of self-correction that formal-verification benchmarks need.\n\nThe evaluation is also thorough by the standards of the field: anti-cheating layers with concrete attack examples, per-instance pass counts, manual inspection of substitutions, and a genuinely informative analysis showing that full solves depend on shared lemma libraries. The finding that the strongest agent passes 87% of individual specifications but fully solves only 27 of 43 repositories is robust in shape, and the implementation-freedom examples (munkres, sortedcontainers) are illuminating.\n\nNow the soft spots, which are real but not fatal. The headline numbers are single-run point estimates with no variance; that is normal for expensive agent evaluations, but it means 27/43 is not a stable ceiling. The larger issue is the one the stress-test note raises: the audit certifies formal satisfiability, not semantic correctness of the 2,705 specifications against upstream intent. The paper concedes this in the limitations section. The 38 repaired defects show that careful manual review still misses things, so residual specification errors could inflate both the \"resists all configurations\" count and the solve ceiling. That said, the authors do about as much as is feasible — Track 1 specifications are cross-checked against source-language formalizations, Track 2 against documentation and tests, and the audit catches unsatisfiable specifications. Semantic fidelity is load-bearing, but the authors know it and have built the best available check. Minor points: the released benchmark is not pinned to a commit hash in the paper, and the cost numbers in Appendix E.4 label 223 of 344 runs as estimated. Neither undermines the benchmark.\n\nThis paper is for people building or evaluating verified code generation agents, and for benchmark designers who care about benchmark defects masquerading as agent failures. It deserves serious peer review, and the reader's CONDITIONAL verdict is about right. I would accept with requested revisions on the repo hash and variance caveats, and I would cite it if I worked on verified code generation.","headline":"Vero is a genuinely new, carefully built repository-level benchmark for verified code generation, and the exact solve counts matter less than the reproducible measurement and the honest audit trail.","tokens_in":27508,"tokens_out":2211,"would_cite":true,"duration_ms":24725,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Vero is the first repository-level benchmark for joint code-and-proof synthesis, and the strongest agent fully solves only 27 of 43 instances.","keywords":["verified code generation","formal verification","Lean 4","AI coding agents","repository-level benchmark","proof synthesis","implementation synthesis","benchmark audit"],"falsifier":"Have an independent team rewrite the specifications for a random sample of instances straight from the upstream documentation and tests, then rerun the strongest agent; if many previously unsolved repositories flip to solved (or solved ones flip to unsolved), the measured capability gap is partly an artifact of specification wording. A sharper check: for the ten instances that resist all eight configurations, provide a human-written lemma library for the missing shared invariants and see whether the same agents then close the repositories; if they do not, the bottleneck is not organization but something else.","tokens_in":26522,"feed_emoji":"🤖","tokens_out":8161,"duration_ms":81581,"temperature":0.7,"pith_summary":"Vero is a benchmark that asks AI coding agents to produce an entire Lean 4 repository from fixed API signatures and manually written specifications, rather than a single function or a supplied implementation. The paper's central claim is that this joint implementation-and-proof task is the right unit of measurement for trustworthy AI-generated software, and that current agents are not ready for it: the strongest configuration fully solves 27 of 43 instances in code-and-proof mode, and 10 instances resist all eight configurations. The authors show that the bottleneck is not local proof skill, since the best agent passes about 87% of individual specifications, but repository-scale organization—discovering shared invariants and building reusable lemma libraries. To keep benchmark defects from masquerading as agent failures, Vero includes a formal audit route that accepts machine-checked negative evidence and uses it to repair specifications.","feed_headline":"Strongest AI agent verifies only 27 of 43 code repositories","feed_subtitle":"Passing 87 percent of individual proofs is not enough; whole-repo proofs stall without shared lemma libraries.","key_machinery":"The central mechanism is the RepoImpl interface structure: every API signature is a field of one structure and each specification is a predicate over that structure, not over a fixed function. Because the proof target can be swapped from the reference implementation to the agent's own code, the same instance supports both task modes and the audit path. The formal audit mechanism accepts three forms of machine-checked negative evidence—an unsatisfiable individual specification, a reference implementation that violates a specification, and inconsistent specification sets—and routes them to curator repair, which during development surfaced 38 adjudicated defects across 9 instances.","core_discovery":"Vero claims to be the first repository-level benchmark that evaluates agents on jointly synthesizing implementations and machine-checked Lean 4 proofs. Each of its 43 instances is a multi-module project frozen around a fixed interface structure: all API implementations are fields of a single RepoImpl structure, and every one of the 2,705 specifications is a proposition parameterized over that structure. This makes proof-only and code-and-proof modes two instances of the same format, and it lets the audit mechanism switch the proof target to a formal counterexample. Empirically, agents pass most specifications in isolation but rarely finish a repository: full solves require cross-module invariants and helper lemma libraries, and the ten unsolved repositories mark the current frontier.","pith_inferences":["A natural next step is to add complexity specifications, since agents already trade asymptotic efficiency for provability when the proof obligation is the binding constraint.","The audit mechanism should run continuously after release: stronger future agents will keep producing negative proofs that expose new latent benchmark errors, so the benchmark and the agents can improve together.","The observed pattern that agents freeze their implementations early and then grind on proofs suggests a testable design change: an agent that revisits its definitions after repeated failures on a bridging lemma would likely close more hard repositories.","Porting Vero to another proof assistant would test whether the gap between per-specification and per-repository success rates is about repository organization generally or about Lean specifically."],"forward_implications":["Because roughly 87% per-specification pass rates leave most repositories unfinished, full-repository verification should be scored as an all-or-nothing property rather than by partial coverage.","Reusable helper lemmas carry most of the proof text in completed repositories, so agent designs that explicitly plan shared lemma libraries should be the next target for improvement.","Implementation freedom helps only the strongest agents; weaker configurations spend their budget on the extra implementation obligation and finish fewer repositories, so code-and-proof and proof-only measure different capabilities.","Without the formal audit mechanism, the 38 latent specification defects found during curation would have been misattributed to agent failures, so benchmark quality depends on formal negative evidence.","Ten instances and 219 specifications resist every tested configuration, giving a concrete, inspectable frontier for future work."],"supporting_citations":[{"why":"Defines the function-level Lean benchmark that Vero extends to whole repositories.","marker":"[20]"},{"why":"Shows the individual-function unit of verified code generation that repository-level evaluation must move beyond.","marker":"[8]"},{"why":"Supplies the closest prior art: a repository-scale Lean benchmark that fixes implementations and evaluates proof only.","marker":"[31]"},{"why":"Represents repository-scale proof-only evaluation in another language, the format Vero's joint code-and-proof mode extends.","marker":"[39]"},{"why":"Another repository-scale proof-only benchmark that helps establish the prior state of the field.","marker":"[33]"},{"why":"Documents latent errors in formal-verification benchmarks, motivating Vero's audit mechanism.","marker":"[10]"},{"why":"Raises contamination risk from public reference solutions, motivating Vero's novel Lean formalizations.","marker":"[14]"},{"why":"Quantifies how pretraining contamination distorts code benchmarks, supporting Vero's structural contamination argument.","marker":"[26]"}],"fun_headline_variants":["AI agents verify only 27 of 43 code repositories","Repository-scale verified coding: AI still falls short","Vero benchmark: Best AI solves just 27 of 43 repos","Whole-repo verification stalls without shared lemma libraries"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The benchmark's conclusions stand on the assumption that the 2,705 manually curated Lean 4 specifications faithfully encode what the upstream programs are supposed to do; the audit mechanism can certify formal satisfiability, but it cannot certify that a satisfiable specification is the right one.","fun_headline_variants_meta":{"raw":{"variants":["AI agents verify only 27 of 43 code repositories","Repository-scale verified coding: AI still falls short","Vero benchmark: Best AI solves just 27 of 43 repos","Whole-repo verification stalls without shared lemma libraries"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000346,"raw_usage":{"total_tokens":1918,"prompt_tokens":987,"completion_tokens":931,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":603,"completion_tokens_details":{"reasoning_tokens":865}},"tokens_in":603,"tokens_out":931,"duration_ms":8783,"temperature":1.0,"reasoning_tokens":865,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T05:05:14.075651+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Have an independent team rewrite the specifications for a random sample of instances straight from the upstream documentation and tests, then rerun the strongest agent; if many previously unsolved repositories flip to solved (or solved ones flip to unsolved), the measured capability gap is partly an artifact of specification wording. A sharper check: for the ten instances that resist all eight configurations, provide a human-written lemma library for the missing shared invariants and see whether the same agents then close the repositories; if they do not, the bottleneck is not organization but something else.","supporting_citations":[{"cited_title":"cp” = code-and-proof, “po","cited_arxiv_id":null,"evidence_quote":"Represents repository-scale proof-only evaluation in another language, the format Vero's joint code-and-proof mode extends."}],"review_version":1}