When ‘Verified’ AI Code Proves Less Than It Seems

Three questions behind one reassuring word

Calling AI-generated code “verified” can obscure what was actually proved. In Verified but Vacuous: Three Failure Surfaces of LLM-Driven Verified Code Generation, Aditya Vempaty and six co-authors argue that a single verification percentage is an inadequate description of a code-generation pipeline’s guarantees.

The supplied source is version 1 of an arXiv preprint, posted on November 3, 2026. Its findings should be read as author-reported research, not established conclusions from peer review.

Formal verification checks whether code satisfies specified obligations under stated assumptions. It does not automatically establish that those obligations express the user’s intention. The paper separates three questions:

• Surface A: verifier acceptance. Did the proof checker accept the generated program?
• Surface B: syntactic specification binding. Does the program’s contract reference the separately defined specification, under the architecture being studied?
• Surface C: semantic specification fidelity. Does the specification capture the intended behavior?

The researchers audit these stages on successively filtered populations. That evaluation sequence does not make the underlying properties a logical hierarchy.

Acceptance without the expected contract

For the first demonstration, the authors reproduced an earlier Dafny-based code-generation approach using Claude Opus 4.7. Their reproduction, called Li@Opus, generates Dafny as an intermediate language before producing Python.

On HumanEval, Dafny accepted 1,625 of 1,640 attempted samples: 99.1% verifier acceptance. Among those accepted samples, only 1.9% passed the authors’ external-specification binding check. Just 5.3% contained any ensures clause—a postcondition describing what must hold after a method finishes.

The reproduction’s prompting convention helps explain the result. According to the paper, its examples use runtime expect statements that Dafny assumes during verification rather than proves. Verification still checks applicable static obligations, but does not thereby prove those runtime expectations or a general functional postcondition.

The authors explicitly describe this as a problem with how the evaluation metric is interpreted, not a defect in the reproduced pipeline. Across three Python benchmarks, verifier acceptance ranged from roughly 92% to 99%, while the conditional binding rate remained between 1.9% and 2.7%.

A structural check, not a meaning detector

The proposed “ensures-binding gate” checks that a method has at least one postcondition referencing a predicate or function declared in its paired specification files. The authors report that this static check takes less than 10 milliseconds per component in their runs.

Its limits are important. A meaningful contract written directly inside a method can fail because it references no external specification symbol. Conversely, a named predicate that always returns true can pass. The gate checks a particular structural convention, not whether a contract is useful or correct.

Consider a task requiring the maximum value in a list. A specification that merely requires a non-negative answer could permit zero for [5, 3, 7]. Proving compliance with that weak specification would not prove that the program returns the maximum.

Linked specifications still leave failures

The second demonstration examines the authors’ own pipeline, VCG, on two Rust benchmarks. In this configuration, every component of a fully verified sample ships with an accepted Dafny certificate that passes the binding gate; no unverified glue is shipped.

Nevertheless, 124 of 1,080 fully verified MBPP-Rust samples failed hidden tests, or 11.48%. On the LeetCode portion of VeriContest, 229 of 1,545 fully verified samples failed, or 14.82%. These percentages concern the fully verified subsets, not all generation attempts.

The authors treat these failures as an operational proxy for requirement fidelity, subject to trusted translation, correct test oracles and semantics-preserving wrappers. The aggregate results do not uniquely identify faulty specifications: translation, composition, implementation, harness or resource problems would need to be excluded when diagnosing individual failures.

VCG also achieved a reported 7.79% end-to-end rate, 535 of 6,870 attempts, on VeriContest’s LeetCode slice. That evaluation includes checks on executable postconditions using positive and negative cases. External comparison rates came from another paper, with unmatched budgets, repair procedures and harnesses; they do not establish a controlled performance advantage.

What the evidence supports

All primary experiments used one model backend, and the main results provide point estimates without confidence intervals. Some Python outputs were excluded from downstream testing after compilation or harness failures. Finite behavioral tests also cannot establish correctness on every possible input.

The practical recommendation is narrower than abandoning verification: report what a certificate binds to and how its specification was evaluated, alongside whether the verifier accepted it. A proof remains valuable—but its meaning depends on the obligations actually proved.