When asking what “verified” should mean for LLM‑generated code, many pipelines report a single verification number. We argue that this collapses three distinct properties measured in a conditional audit sequence:
- Surface A: verifier acceptance, i.e., whether the generated code passes a formal verifier;
- Surface B: syntactic specification binding, i.e., whether the proof obligation actually binds to a spec‑defined predicate or function;
- Surface C: semantic specification fidelity, i.e., whether the spec fully captures the informal requirement.
Experiment 1 (A ≠ B): Using Li@Opus (a same‑model reproduction of \citet{li2025dafny}'s Dafny‑IR pipeline under Claude Opus 4.7) on three Python benchmarks, we achieve 99.1% verifier acceptance on HumanEval but only 1.9% of the samples carry a certificate that binds to a spec‑defined predicate, showing that high acceptance does not guarantee spec binding.
Experiment 2 (B ≠ C): We apply VCG (our in‑house Dafny‑IR pipeline) on two Rust benchmarks. The Rust target forces every component to ship as a Dafny certificate, ensuring the binding gate passes by construction. Nevertheless, 11.48% (MBPP‑Rust) and 14.82% (VeriContest LC slice) of structurally verified samples still fail hidden tests, indicating that the spec does not faithfully capture the informal requirement.
On the LC slice of VeriContest, VCG reports an End‑to‑End rate of 7.79% (535/6870). External rates are 5.51% for GPT‑5.5 and 1.88% for single‑shot Opus 4.7. The descriptive differences are 2.3 percentage points and $4.14\times$, respectively; differences in task budget, repair strategies, and harness prevent a matched‑performance claim.
Review: These three failure surfaces remind us that pursuing formal verification of LLM‑generated code requires more than a high verifier acceptance rate. We must also ensure that the code is properly bound to a meaningful specification and that the specification itself faithfully represents the intended behavior, otherwise the “verification” may be merely superficial.