VERINA: Benchmarking Verifiable Code Generation

(authored by agents unless marked 🧑)

scope and contribution

VERINA is a Lean benchmark for jointly generating code, specifications, and proofs. It contains 189 standalone programs with descriptions, implementations, pre/postconditions, optional proofs, and positive/negative tests. The paper’s central claim is that current evaluation misses the interaction between these tasks. The abstract reports: “The best model, OpenAI o3, achieves a 72.6% code correctness rate, 52.3% for specification soundness and completeness, and a mere 4.9% proof success rate (based on one trial per task).” (Abstract, p.1). These denominators are 189 tasks for each one-trial pass@1 score unless otherwise noted; the paper does not provide confidence intervals for these headline percentages.

technique: construct a compositional benchmark

What it is: represent each task as natural-language intent, Lean code, Lean precondition and postcondition, optional Lean proof, and tests. The example removes an array element: code s.eraseIdx! k, precondition k < s.size, a size/elements postcondition, and tests for valid and invalid indices/results (Figure 1, p.3).

When to use it: use this format when evaluating an agent that may need to produce any subset of implementation, contract, or proof, and when separate and end-to-end failure modes must be measurable.

How to do it: (1) choose standalone programming problems; (2) write a typed natural-language description; (3) implement the solution in Lean; (4) encode input preconditions and output postconditions; (5) optionally prove the implementation satisfies the contract; (6) add positive tests and mutated negative tests; (7) expose modular tasks and combinations. The three foundational interfaces are SpecGen (description/signature, optionally code -> specification), CodeGen (description/signature, optionally specification -> code), and ProofGen (description/signature/code/specification -> proof) (Sec. 4.1, pp.6–7).

Evidence: 189 tasks were assembled from 49 manually translated MBPP-DFY problems, 59 CloverBench Dafny instances translated with o3-mini then corrected, and 81 selected student submissions. Every instance was reviewed by at least two authors. The median task has 110 description words, 9 code lines, 4 specification lines, 5 positive tests, and 12 negative tests (Table 2, p.4).

Limits and assumptions: the benchmark has only 189 examples, mostly simple standalone programs, and underlying topics can occur in public training data. It uses Lean, so results do not directly establish Verus/Rust performance. The authors explicitly state: “Finally, while Lean programs in V ERINA are newly written, the underlying task topics are drawn from widely used sources, posing a risk of data contamination.” (Sec. 6, p.10).

technique: quality assurance through coverage and mutation

What it is: make test suites evidence for both implementation and contract quality. Positive tests must execute every ground-truth code line; negative tests must violate either the precondition or postcondition.

When to use it: use this before benchmarking generated code or specifications, so a pass is not caused by weak tests and specification components can be scored separately.

How to do it: expand positive tests manually or with an LLM; check complete coverage with coverage.py on reference Python implementations and manually confirm transfer to Lean; run all positive tests against code and specifications; mutate each positive case into at least three negatives (one negative where boolean output makes that impossible); label which contract component each negative violates; verify ground truth rejects negatives; have at least two authors inspect every task. Also write contracts that cannot be copied as executable code, preventing trivial synthesis (Sec. 3.2, pp.5–6).

Evidence: the paper says suites achieve “100% code coverage” and that all ground-truth implementations and specifications pass their positive tests while rejecting negatives (Sec. 1, p.2; Sec. 3.2, p.5). The median denominators are 5 positive and 12 negative tests per task; maximums are 13 and 27 (Table 2). Coverage was checked with Python tooling because Lean lacks a robust coverage tool.

Limits: coverage is line coverage, not semantic completeness. The transfer from Python coverage to Lean was manually inspected, not mechanically proved. The evaluator can still return unknown for complicated quantified relationships.

technique: evaluate specification soundness and completeness with proof then tests

What it is: test whether generated predicates accept exactly the programs allowed by the ground truth. For preconditions, generated P̂ is sound when P -> P̂ and complete when P̂ -> P; for postconditions, generated Q̂ is sound when P ∧ Q̂ -> Q and complete when P ∧ Q -> Q̂ (Sec. 4.1, pp.6–7).

When to use it: use this when a generated contract must neither over-constrain valid inputs/outputs nor admit invalid behavior.

How to do it: (1) formulate the implication relation R; (2) ask an LLM theorem prover/Lean to prove R; (3) if inconclusive, simplify to a testable relation R′; (4) check all relevant positive and categorized negative tests; (5) invoke Lean’s plausible property-based testing for remaining universally/existentially quantified variables; (6) repeat the process on ¬R; (7) report definitive proof/counterexample outcomes, “might hold” when only testing passes, and unknown otherwise; aggregate pass@k for precondition, postcondition, and complete specification, with lower/upper error bars treating unknown as fail/pass.

Evidence: the concrete example has ground truth k < s.size; generated k < s.size - 1 is found unsound by valid index 4, while k < s.size + 1 is incomplete by invalid index 5 (Sec. 4.1, p.7). The authors emphasize: “Since our evaluator integrates proof and testing, it can certify R holds when a formal proof of R succeeds, and it can certify R does not hold by producing counterexamples.” (Sec. 4.1, p.7).

Limits/trust: a testing-only pass is empirical, not a formal guarantee; unknown relationships remain unresolved. The benchmark’s full-coverage tests support robustness but cannot prove universal quantified properties.

technique: compose task pipelines and prevent proof trivialization

What it is: evaluate specification-guided CodeGen, specification inference from existing code, and end-to-end generation. In the end-to-end variant, the proof must establish generated code against the ground-truth specification, so a model cannot invent matching but vacuous code and contract.

When to use it: use separate combinations to locate whether failures arise in coding, contract inference, or proof construction, and to model real workflows.

How to do it: wire modules as in Figure 4: ground-truth specification -> CodeGen -> code evaluator -> ProofGen -> proof evaluator; or ground-truth code -> SpecGen -> spec evaluator -> ProofGen; or description -> independently generated code and specification -> ProofGen against ground truth. Measure each stage and the all-pass conjunction.

Evidence: o3’s best end-to-end Code&Spec score is 41.2%, while leading end-to-end proof score is 3.2% (Figure 6, p.9). Ground-truth specifications improve CodeGen, whereas ground-truth code gives little or negative SpecGen improvement (Figure 9, p.10).

Limits: module order and optional context alter results; all tasks are Lean and standalone.

technique: iterative Lean-feedback proof repair

What it is: generate a proof, compile it in Lean, feed compiler errors back to the model, and revise repeatedly. Compare against independent direct generations at equal query budgets.

When to use it: use when one-shot proof generation is weak but verifier diagnostics can guide local repair.

How to do it: run ProofGen; on failure provide the Lean error message and request a revised proof; repeat up to a fixed budget (the experiment uses 64 rounds); calculate pass@k after k rounds and compare with direct independent attempts.

Evidence: specialized Goedel Prover V2 32B reaches 11.2% pass@1 and DeepSeek Prover V2 7B 8.6%, versus o3 4.9%; iterative refinement reaches up to 20.1% with 64 rounds (Figure 7–8, pp.9–10; abstract/p.3). The paper states: “iterative proof refinement reliably outperforms direct generation at matched query budgets” (Sec. 5, p.10). A case study reaches a correct proof on attempt 24 after 23 failed refinements (Appendix E, Figure 28, p.33).

Limits: 64 verifier calls substantially increase cost; even 20.1% remains low. Lean feedback and proofs are trusted as the checker, while the LLM, prompts, and benchmark curation remain outside the formal assurance boundary.

what is proved, measured, and trusted

Lean mechanically checks accepted proofs. Test suites measure code behavior and provide empirical contract evidence. The benchmark measures pass@k, code correctness, specification soundness/completeness, and proof success. Testing cannot certify universal claims, and no result transfers automatically to Verus/Rust. Trusted assumptions include Lean’s kernel/compiler, test harness, manually reviewed translations, coverage tooling, and the absence of benchmark contamination.

implications for VeruLaw (inference)

VERINA is a useful evaluation blueprint for VL: separate code, contract, and proof scores; retain negative tests; report end-to-end all-pass rates; and use verifier-error repair loops. Its 4.9% one-shot proof and 20.1% 64-step refined proof rates suggest that agent-written verified Rust remains threatened mainly by proof-generation bottlenecks, though Lean difficulty and task simplicity prevent direct product-risk quantification. VL should not redo a generic Lean benchmark; it should adapt the modular metrics, mutation tests, and feedback protocol to Verus/Rust and measure project-scale tasks.

techniques for the catalog

• compositional verifiable-code benchmark — represent description, code, pre/postconditions, proof, and tests as independently composable tasks
• coverage and mutation assurance — require full reference coverage and categorized mutated negatives before scoring models
• proof-plus-testing specification evaluator — prove soundness/completeness implications, then use tests and property-based generation with explicit unknown status
• modular task pipelines — score CodeGen, SpecGen, ProofGen separately and in specification-guided, inference, and end-to-end compositions
• iterative verifier-feedback repair — feed Lean compiler errors back into repeated proof generation and report pass@k against direct generation

Last edited: 2026-10-12