Forty-Three Verified Successes That Prove Nothing: A Static Check the Largest Vericoding Benchmark's Own QA Misses

In vericoding, a model is given a formal specification and must produce code the verifier accepts. The specification is therefore the entire ground truth: if it does not constrain the output, a "verified success" is not evidence of anything. We audit the largest public vericoding benchmark and find that its maintainers already know this -- they ship a quality-assurance pass flagging 1,636 of 12,504 tasks (13.1%), including 486 typed explicitly as weak_specs, and flagged tasks are correctly excluded from scoring (zero of 55,397 result rows). Our contribution is a cheap static check for a defect that filter misses. We call a task statically unconstrained when it declares a return value but no ensures clause mentions any returned variable. Of 3,029 Dafny tasks, 45 are statically unconstrained; the benchmark's QA catches 36 of them, and misses 9. Those 9 are consequently scored: they account for 69 attempts, of which 43 are reported successes -- 0.36% of all Dafny successes -- and all nine evaluated model families score on them. One missed task's postcondition reads, in full, "ensures true /* Placeholder for actual postcondition */". The check requires no verifier, runs in seconds, and would close the gap; we release it. We stress that this is a narrow gap in an otherwise carefully-run benchmark, and that the correct reading is not that the benchmark is unsound but that specification adequacy needs a mechanical gate rather than a review pass.