Beyond `assume false': Residual Reward Hacking in Verified-Code Harnesses

Verified-code benchmarks certify a generated program by running a verifier and then screening the artifact with a cheat checker: a blocklist of the bypasses its authors observed, such as assume false, sorry, {:verify false}, or non-whitelisted axioms. We show these checkers are reactive and incomplete. Residual channels remain — rooted in language semantics and checker scope rather than in implementation bugs — through which an artifact passes a community-standard harness while failing an independent, machine-checkable correctness check. We contribute: (1) a mechanism-level taxonomy of residual channels spanning Dafny, Verus, and Lean: nontermination and partial-correctness opt-outs, runtime-halt-as-verified, verified-versus-executed divergence, spec-dependency mutation, statement re-elaboration, and checker-scope gaps; (2) certified exploits, pairing a harness-accepted artifact with a machine-checkable witness of a channel-specific correctness failure, with no model-as-judge in the evidence chain; (3) hackability@budget, a per-harness robustness metric: the fraction of tasks on which a fixed-budget red-team agent wins acceptance without a correct implementation; (4) an optimization-pressure study (best-of-n, GRPO) of channel discovery and the resulting pass-to-correct gap; and (5) a hardened checker, its measured cost on honest solutions, upstream-oriented fixes, and a trusted-base reporting convention. We measure pooled hackability@budget up to 39.1% (DafnyBench), a gap of 30.2 pp between training reward and held-out correctness under standard-checker reinforcement learning, and honest-solution cost at most 6.1%. The checker, not the verifier, defines the reward. All artifacts are provided as anonymized supplementary material, and every finding will be disclosed to maintainers before public release.