Verus 中的正确性反馈为何会抹除证据：阶段分离的完整性审计

View PDF HTML (experimental)

Abstract:Correctness feedback suppresses the very evidence that specification-completeness auditing is designed to uncover: programs that satisfy a written contract but violate intended behavior. We demonstrate this objective reversal on 12 Verus/Rust tasks across four model families under matched call budgets. Independent no-feedback discovery more than doubles certified-witness yield relative to IntentShield's corrective-feedback loop (59.0% versus 27.1%). A format-matched iterative control places the larger share of this gap in feedback content, not independent restarts. The advantage holds in every model family and survives parser repair. A separate phase-separated execution matches the aggregate yield without reusing responses; most certified witnesses also fail held-out cases. Preserving these witnesses delivers stronger specification repair: Phase-Revised contracts achieve 81.3% implementation success, 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.

Comments:	Paper accepted at the NeurIPS 2026 Workshop on AI for Verifiable Coding
Subjects:	Artificial Intelligence (cs.AI)
Cite as:	arXiv:2610.20676 [cs.AI]
	(or arXiv:2610.20676v1 [cs.AI] for this version)
	https://doi.org/10.48550/arXiv.2610.20676 arXiv-issued DOI via DataCite

Submission history

From: Adarsh Agrawal [view email]
[v1] Wed, 14 Oct 2026 14:43:24 UTC (1,388 KB)