Verified but Vacuous: Three Failure Surfaces of LLM-Driven Verified Code Generation

Aditya Vempaty; Himaneesh Sompalle; Manan Tayal; Mowafak Allaham; Prasenjit Dey; Ashish Jagmohan; Ravi Kokku

cs.AINov 3, 2026

Verified but Vacuous: Three Failure Surfaces of LLM-Driven Verified Code Generation

Authors: Aditya Vempaty, Himaneesh Sompalle, Manan Tayal, Mowafak Allaham, Prasenjit Dey, Ashish Jagmohan, Ravi Kokku

Abstract

What should ``verified'' mean when evaluating LLM-generated code? Many existing pipelines report a single verification number. We argue this collapses three distinct properties measured in a conditional audit sequence: verifier acceptance (Surface A), \emph{syntactic specification binding (Surface B: does the proof obligation bind to the spec?), and semantic specification fidelity (Surface C: does the spec capture the informal requirement?). Two empirical demonstrations show the surfaces separate. \textbf{First ( $A \neq B$ ), via Li@Opus (a same-model reproduction of \citet{li2025dafny}'s Dafny-as-intermediate-representation (IR) pipeline under Claude Opus 4.7) on three Python benchmarks}: it reaches 99.1% verifier acceptance on HumanEval while only 1.9% carry a certificate binding to a spec-defined predicate or function. \textbf{Second ( $B \neq C$ ), via VCG on two Rust benchmarks}: we use VCG (which is our own in-house Dafny-as-intermediate pipeline) on Rust because the Rust target lets us enforce fully-verifiable output (every component ships as a Dafny certificate, ensures-binding gate passing by construction). Even inside that construction, 11.48% (MBPP-Rust) and 14.82% (VeriContest LC slice) of structurally-verified samples still fail hidden tests. On the LC slice of VeriContest, VCG's reported End2End rate is 7.79% (535/6870). The cited external rates are 5.51% (GPT-5.5) and 1.88% (single-shot Opus 4.7). These give descriptive differences of 2.3 percentage points and 4.14 $\times$ , respectively; task-budget, repair and harness differences prevent a matched-performance claim.

Figures & tables

Surface	Check	Catches	Blind spot (deferred)
A: verifier acceptance	dafny verify (or verus ) exits zero	proof gaps, type errors, missing lemmas	vacuous or absent ensures clauses
B: syntactic spec binding	some ensures clause references a spec-defined predicate / function	missing references to the paired spec artifact, including meaningful inline contracts	semantically weak predicates that bind but under-specify
C: semantic spec fidelity	postcondition accepts positive tests and rejects negatives (Post2Exe)	weak specs whose predicates admit incorrect outputs	requirements no test suite happens to exercise

Table 1: The audit stages use conditional populations. Verifier acceptance, external-reference checking and finite behavioral probes measure distinct properties; the stages are not a logical hierarchy.

Benchmark	# problems	Samples/prob.	Target	Source
HumanEval / HumanEval+	164	10	Python	( Chen et al., 2021 ; Liu et al., 2023 )
LeetCodeDataset	228	10	Python	( newfacade, 2024 )
LiveCodeBench v6	1,055	10	Python	( Jain et al., 2024 )
MBPP-Rust	208	10	Rust	( Emergence AI, 2026 )
VeriContest LC slice	687	10	Rust	( Xie et al., 2026 )

Table 2: Benchmarks used in this study. Samples/prob. is 10 across all VCG, BareLLM, and Li@Opus runs; the VeriContest authors’ reported per-slice Opus 4.7 End2End LC number (1.88%; our same-backend comparator in § 6 ) is single-shot per problem.

	HumanEval	LeetCodeDataset	LCB v6
Total samples (attempted)	1,640	2,280	10,550
Level 1: verifier-accepted (denom.)	1,625	2,217	9,731
Level 2: any ensures clause	5.3%	9.6%	10.61% ∗
Level 3: ensures-binding gate passes	1.9%	2.7%	2.3%

Table 3: Certificate quality on Li@Opus, Claude Opus 4.7, three Python benchmarks. Level-2 and Level-3 rates are conditional on verifier acceptance (Surface A); raw dafny verify pass rates are

99.1\%\,/\,97.2\%\,/\,92.2\%

	(i) Hidden-test failure	(ii) Post2Exe
Question asked	Does the implementation match the requirement?	Does the postcondition itself match the requirement?
Mechanism	Run the shipped code against hidden tests	Translate the postcondition to an executable predicate; check it accepts positives and rejects negatives
Reported in	Table 5 (both Rust benchmarks)	End2End @1 (VeriContest LC)

Table 4: Two Surface-C instances reported in this paper. Both condition on samples that have already cleared Surfaces A and B. They ask different questions and can catch different failure modes.

Benchmark (Rust)	Total attempts	Fully-verified	$B\to C$ fails	$B\to C$ failure rate
MBPP-Rust ( Emergence AI, 2026 )	2,080	1,080	124	11.48%
VeriContest LC ( Xie et al., 2026 )	6,870	1,545	229	14.82%

Table 5: VCG on the two Rust benchmarks. Fully-verified samples pass our Surface-B (ensures-binding) criterion by construction and ship a dafny verify -accepted certificate on every component.

B\to C

failure rate is the fraction of those that nonetheless fail hidden tests, a Surface-C proxy under the trusted-toolchain and correct-oracle assumptions. Unconditional failure rate is the same failure count expressed as a share of all attempts (10 samples per problem: 5.96% on MBPP-Rust, 3.33% on VeriContest LC).

Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 1 — Figure 1: Two pipelines fall out of the cascade at different surfaces. Bar widths are proportional to the fraction of attempted samples surviving each surface (HumanEval: 1640 attempts; VeriContest LC: 6870 attempts). Li@Opus’s collapse is at $A\to B$ (99.1% verifier acceptance, but only 1.9% carry a certificate binding to a spec-defined predicate). VCG closes B on 100% of A by construction; its collapse is at $B\to C$ (22.49% dafny verify passing to 7.79% End2End @1). A pipeline reporting only Surface A would show 99.1% and 22.49% respectively for Li@Opus and VCG and hide the shape of failure in both cases.

System	Surface A	Surface B (syntactic binding)	Surface C (semantic fidelity)
Li et al. (2025)	Yes	Not reported	Runtime fixtures only
VeriContest ( Xie et al., 2026 ) end-to-end	Yes	Not reported	Post2Exe on postcondition
AxDafny ( Breen et al., 2026 )	Yes	Missing/trivial ensures , {:axiom} , LLM reviewer	Not reported
VCG (our own)	Yes	Ensures-binding gate	Hidden-test proxy on Rust runs; Post2Exe applied on VeriContest LC (7.79% End2End @1, 535/6870)

Appendix

Table 6: What existing pipelines and evaluations report on each surface. Most systems that report Surface A do not report either companion surface.

Benchmark (Python)	With ensures	Without ensures	Delta
HumanEval (base tests)	80.2% ( $n=86$ )	94.2% ( $n=1{,}539$ )	$-14.0$ pp
LeetCodeDataset	59.6% ( $n=213$ )	66.1% ( $n=1{,}995$ )	$-6.5$ pp
LiveCodeBench v6	53.2% ( $n=1{,}032$ )	62.6% ( $n=8{,}416$ )	$-9.4$ pp

Appendix

Table 7: Pass rate by presence of ensures clause on test-evaluated samples, Li@Opus, three Python benchmarks (excluding 9 LeetCodeDataset and 283 LiveCodeBench v6 compilation/shimming dropouts). Samples with an ensures clause pass hidden tests less often than samples without one on every benchmark; this observational association among self-selected outputs does not identify a causal effect of writing specifications.

Code Generation Evaluation

Code generation evaluation measures whether AI-produced programs are correct, reliable, secure, efficient, and faithful to their specifications.

See all 220 papers

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation
Aug 10, 2026Zenan Li, Ziran Yang, Peiyang Song +2Code Generation Formal Verification
1Apodex · 2Princeton University · 3Caltech +1
AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
Apr 24, 2026Pouya Pezeshkpour, Estevam HruschkaLLM Evaluation LLM Answer Verification
Megagon Labs
From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
Apr 24, 2026Md Erfan, Md Kamal Hossain Chowdhury, Ahmed Ryan +1LLM Prompting Code Generation
Department of Computer Science, The University of Alabama, Tuscaloosa, USA · Alabama Water Institute, The University of Alabama, Tuscaloosa, USA

Aug 10, 2026J/K move · Enter open · S save

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation

Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li+1

1Apodex · 2Princeton University · 3Caltech+1

Code Generation Formal Verification Agentic Code Generation Code Generation Benchmarks Verified Code Generation

Open paper AskPDF arXiv

Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouples the two halves of the problem: first synthesize a program, then attempt to prove it correct. We observe that this sequential pipeline can be both ineffective and inefficient in practice. A program generated without anticipating its proof can be subtly incorrect or structurally difficult to verify, forcing the LLM into brittle repair loops that alternate between patching the code and patching the proof. Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose

P^3

, an LLM-based agentic workflow that first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. To evaluate verified code generation in realistic settings, we further introduce Lean4Commit0, a repository-derived, library-level benchmark built by extracting core APIs from real-world software repositories and translating their requirements, including relational specifications across APIs, into Lean tasks. Using four frontier LLM backends, we evaluate

P^3

on Verina, AlgoVeri, and our Lean4Commit0 benchmark, where it achieves the highest solve rate in every benchmark--model setting. Compared with the stronger baseline, it improves solve rates by 4.6--11.2 percentage points and reduces per-task API cost by up to roughly 40% and wall-clock time by up to roughly 37% on the difficult subset of each benchmark. A targeted ablation further shows gains of 3.3--8.3 points over implementation-only planning, isolating the benefit of planning the program and proof jointly.

Abstract

Code Generation Evaluation

Explore similar work

P3^{3}3: Joint Program-and-Proof Planning for Verified Code Generation

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation