正确性反馈会抹除证据：Verus 中相分离的完备性审计发现模型失效

该研究指出在 Verus/Rust 工作流中，用于纠正错误的“正确性反馈”机制反而会抑制甚至消除那些能暴露规范不完备性的关键证据，导致审计目标发生逆转。实验在四个模型族上匹配调用预算后显示，独立无反馈模式发现的已认证见证数量（59.0%）是 IntentShield 校正反馈循环（27.1%）的两倍以上，且这一优势在所有模型族中均成立并经受住了解析器修复测试。

数据进一步表明，这种差距主要源于反馈内容本身而非独立的重启尝试。通过相分离执行策略保留这些被通常流程过滤掉的见证，显著提升了后续规范修复的质量：Phase-Revised 合同实现了 81.3% 的实现成功率，远高于 IS-Revised 的 62.5%，而 Direct-Revised 紧随其后。值得注意的是，这些被保留的见证在独立测试集上也表现不佳，说明它们确实捕捉到了未被覆盖的失败场景。然而，该效应在现有的 Dafny 和 Lean 评估中未能复现，确立了该结论仅适用于当前研究的 Verus/Rust 特定工作流。

事实层面，研究证实了无反馈模式在特定工具链下具有更高的证据捕获率；推断层面，这意味着当前的自动化审计流程可能因过度追求即时正确性而牺牲了长期的规范完备性；猜测层面，若将此类相分离策略推广至其他语言或框架，可能需要重新设计反馈触发机制以避免类似的信息丢失，但这尚需更多实证支持。