VeriBench: An End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4

Test-based coding benchmarks have repeatedly required strengthening passes (HumanEval, HumanEval+, SWE-Bench, SWE-Bench Verified,SWE-Bench+), each release exposing test-invisible bugs in code that passed the prior suite. This reflects a structural limit of finite testing: passing tests routinely leave behaviorally important bugs unobserved. Existing formal-verification benchmarks (e.g., VERINA, FVAPPS, CLEVER, DafnyBench) provide stronger machine-checkable signals, but many focus on proof completion, scaffolded verified generation, or isolated formal subtasks rather than the full path from developer-written source code to a verified formal artifact. We argue that trustworthy code-verification benchmarks must be end-to-end and agentic, scoring full Python-to-Lean autoformalization under verifier feedback, and must aggregate verification stages conjunctively so that weakness at any stage penalizes the composite while preserving smooth evaluation signal across models still far from the frontier. We introduce VeriBench, an 896-task end-to-end Python-to-Lean4 autoformalization benchmark with a 614-task canonical core (HumanEval-style programs, classical algorithms, Python standard-library functions, and security examples) and a 282-task high-assurance-inspired set across 14 domains including cryptography, aerospace, medical devices, and compilers. We score agents with the Smooth Conjunctive Score for Code verification (SCSC), a log-domain geometric mean over five per-task factors, $\mathrm{SCSC} = \exp\!\bigl(\tfrac{1}{5}\sum_i \log f_i\bigr)$, combining (i) the agent's Lean file typechecks, (ii) the agent's theorems verify without sorry, (iii) the agent's theorems semantically cover the curated reference theorems (an LLM-judge estimate, not a kernel-checked entailment), and (iv,v) reference-side validity gates ($D_1, D_2$) ensuring the curated reference itself compiles and proves cleanly before being used to score agents. Under an agentic verifier-feedback loop, Codex, Claude Code, and Leanstral-v2 reach SCSC of only $0.42$, $0.36$, and $0.23$; iterative self-correction adds $14.3\%$ over single-shot baselines, yet judge-estimated theorem-to-reference coverage stalls uniformly at $\leq 0.11$ across all three agents, a candidate specification gap corroborated by an LLM judge calibrated against five independent human raters (Pearson $r=0.70$, $p<10^{-11}$). VeriBench frames code-verification evaluation as end-to-end conjunctive grounding, surfacing specification synthesis as a candidate bottleneck at least as severe as proof search and offering a measurable target for verifiable AI coding agents.