LLM Verification Co-Evolution Underperforms a Deterministic Allocator on a Ten-Design RTLLM Audit

LLM-driven RTL verification generators optimising against their own preference distribution risk silently losing hidden mutants and missed properties as they improve. We measure five candidate systems — direct prompt, coverage-guided, bounded-formal-only, deterministic-allocator (KR-1: per-design-class strongest deterministic technique — inline templates on combinational, bounded formal miter on sequential), and a co-evolving generator/allocator loop — at matched scalar cost (sim-seconds + SMT-seconds + LLM-token-cost) on 150 pre-registered E1 cells (RTLLM; 7 combinational + 3 sequential) against a hash-verified 6-design sequestered anchor. The pre-registered kill rule FIRES against the adaptive-amended KR-1 baseline (per-design-class strongest deterministic technique; see §Limitations (vi)) and is inconclusive against the formal miter. The 30 design-seed cells come from only 10 designs, so we resample designs with seeds nested: (co-evolve−deterministic-allocator) = [−0.932, −0.087] fires, as does the combinational slice ([−0.570, −0.001]) on which KR-1 shares no machinery with the miter, whereas (co-evolve−bounded-formal-only) = [−1.025, +0.037] straddles zero; both fire at the pre-registered cell level ([−0.742, −0.199], [−0.793, −0.097]). Of the 36 observable mutant-verdicts (12 distinct mutants × 3 seeds) the miter confirms distinguishable, co-evolve catches 25 (69%) — missing nearly a third of definitively-detectable faults — while KR-1 catches all 36. The LLM loop loses on discriminative power AND on cost, and the non-LLM baselines stay cost-competitive at every LLM-token price from $3/1k to $0/1k.