The Refutation Verification Gap in Oracle-Guided Synthesis of Non-Blocking Data Structures

Agentic coding loops are increasingly closed with test oracles rather than verifiers, so a candidate passes through generation, refutation, corroboration and verification while the loop treats the last three as one. The operative question is then not Pass@$k$ but what *passing* certifies. We study it for non-blocking concurrent data structures, where linearizability checking is NP-complete and mechanized proof demands expert guidance, so neither in-loop verification nor ad-hoc testing is available. A repair loop inverts the usual cost of oracle errors: a false negative merely advances a candidate, whereas a false refutation makes the model dismantle correct synchronization. We prove the asymmetry compounds under a no-recovery assumption, measure both of its quantities, and measure that assumption failing. A single false refutation drops survival from $80.6\%$ to $44.4\%$ ($p \approx 0.004$), and over 2018 runs on candidates an independent checker accepts, the sound check commits one at $0.05\%$ per visit, exact interval $[0.001, 0.28]\%$, inside the budget the proposition demands. We formalize two checks and separate their status: *terminal consistency*, a sound refutation oracle for linearizability with a necessity theorem and $O(|\mathcal{K}|+|H|)$ checking, and *bounded terminal lock-freedom*, a calibrated preemption stress test whose refutations hold only modulo a step budget not computable from the implementation. We then measure the residual gap, out of 155 candidates clearing terminal consistency and a progress check, an independent Tier-2 corroborates 136 ($87.7\%$ $[81.5, 92.5]$), and all 19 residual defects are wrong return values over an exact terminal state, fifteen stale reads and four failed removes: a shape a per-operation monitor catches by construction and a terminal one cannot. Decomposing oracle design into contention, observable and schedule exploration, the last buys nothing: at matched scenario and matched budget Lincheck's bounded model checker refutes no candidate its randomized stress mode does not, while stress refutes 54 it misses. On the generators, all six open-weight and commercial models score $0.00$ on descriptor-based binary search trees zero-shot in both languages, and the one prompting regime that appears to beat this emits trees with no descriptor protocol at all. We release NB-Bench and the full per-candidate record.