Correctness feedback suppresses the evidence that specification‑completeness auditing is meant to uncover: programs that meet a written contract but violate the intended behavior. We evaluated 12 Verus/Rust tasks across four model families under equal call budgets and found that independent no‑feedback discovery yields a certified‑witness rate of 59.0%, compared to 27.1% for IntentShield’s corrective‑feedback loop. A format‑matched iterative control shows that most of this gap stems from the feedback content rather than independent restarts. The advantage persists across all model families and survives parser repair. A separate phase‑separated execution matches the aggregate yield without reusing responses, although most certified witnesses still fail held‑out cases. Preserving these witnesses enables stronger specification repair: Phase‑Revised contracts achieve an implementation success rate of 81.3%, versus 62.5% for IS‑Revised, with Direct‑Revised close behind. Both no‑feedback witness sources substantially outperform weakened contracts. The effect does not reproduce in the available Dafny and Lean evaluations, establishing an empirical boundary around the studied Verus/Rust workflow. Completeness auditing and correctness repair have opposing immediate objectives: preserve and certify the admitted failure before repairing it.
Review