正确性反馈会抑制规范完整性审计本应揭示的证据：即满足书面合约却违背预期行为的程序。我们在 12 项 Verus/Rust 任务上，对四类模型在相同调用预算下进行实验，发现独立的无反馈发现能够将认证证据产出提升至 59.0%，而 IntentShield 的纠正反馈循环仅为 27.1%。采用格式匹配的迭代对照实验表明，差距主要来源于反馈内容而非独立重启。该优势在所有模型族中均成立，并且在解析器修复后仍然存在。另一种相位分离的执行方式在不复用响应的前提下实现了相同的整体产出；然而大多数认证证据在持出测试中仍会失效。保留这些证据能够显著提升规范修复的效果：相位修订合约的实现成功率达到 81.3%，而 IS‑修订为 62.5%，Direct‑修订略低但仍接近。两种无反馈证据来源均显著优于弱化合约的表现。相同实验在 Dafny 与 Lean 环境中未能复现，划定了本研究所关注的 Verus/Rust 工作流的经验边界。完整性审计与正确性修复的直接目标相互冲突：在修复之前应先保留并认证已发现的失败。
点评