AI News

This study examines whether correctness feedback helps or harms specification-completeness auditing in Verus/Rust programs. Across 12 tasks and four model families under matched call budgets, independent no-feedback discovery produced certified witnesses in 59.0% of cases, compared with 27.1% for IntentShield’s corrective-feedback loop. A format-matched iterative control attributed most of the gap to the content of the feedback rather than to independent restarts, and the advantage appeared in every model family and remained after parser repair. A phase-separated execution that did not reuse responses matched the aggregate yield, showing that response reuse was not required. Most certified witnesses nevertheless failed held-out cases. Preserving the witnesses before repair improved specification repair: Phase-Revised contracts reached 81.3% implementation success, compared with 62.5% for IS-Revised, while Direct-Revised was close behind; both no-feedback sources outperformed weakened contracts. The effect was not reproduced in the available Dafny and Lean evaluations, limiting the claim to the studied Verus/Rust workflow. The authors conclude that completeness auditing and correctness repair have opposing immediate goals, so discovered failures should be preserved and certified before contracts are repaired.