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

What should “verified” mean when evaluating LLM-generated code? Many existing pipelines report a single verification number (for example, dafny verify accepted N% of samples). We argue this collapses three properties that are logically nested and empirically separable: verifier acceptance (Surface A), 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?). We contribute this three-surface decomposition plus the ensures-binding gate, a syntactic Surface-B instance for Dafny pipelines that emit distinguishable specification and implementation artifacts (static AST walk, $<10$ ms per component). Two empirical demonstrations show the surfaces separate. First ($A\ne B$), via Li@Opus (a matched-model reproduction of li2025dafny's Dafny-as-intermediate-representation (IR) pipeline under Claude Opus 4.7) on three Python benchmarks of simple coding tasks (LeetCode-style): it reaches 99.1% verifier acceptance on HumanEval while only 1.9% carry a certificate binding to a spec-defined predicate or function. This gap is roughly fortyfold ($36$ to $52\times$) that holds across HumanEval, LeetCodeDataset, and LiveCodeBench v6 in a narrow 1.9% to 2.7% band. This gap is observed even as the fraction of verified samples that carry any ensures clause climbs from 5.3% on HumanEval to 10.9% on LiveCodeBench v6. Postcondition prevalence more than doubles with benchmark difficulty but binding-to-a-spec-predicate rate does not follow. Second ($B\ne 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.4% (MBPP-Rust) and 14.82% (VeriContest LC slice) of structurally-verified samples still fail hidden tests. On the LC slice of VeriContest, VCG's End2End rate is 7.79% (535/6870) at pass@1, +2.3 pp above the best previously published End2End LC number (GPT-5.5's 5.51%) and 4.14$\times$ the matched-backend single-shot Opus 4.7 End2End LC baseline (1.88%) that the VeriContest authors report per-slice. Therefore, any pipeline shipping certificates should report at least one of Surface B (e.g. the ensures-binding gate) or Surface C (e.g. Post2Exe) alongside Surface A; where feasible, both, since Surface B alone leaves the semantic blind spot we demonstrate on VCG, and Surface C alone leaves the syntactic blind spot we demonstrate on Li@Opus. Many existing evaluations report neither.