正确性反馈会抹除证据：Verus 形式验证中的分阶段完整性审计

研究问题与发现

该预印本（arXiv:2610.20676v1，2026 年 10 月发布）关注规格完整性审计中的一个矛盾：程序满足书面契约，却仍可能违反预期行为，而正确性反馈恰恰会压制揭示这类问题的证据。作者在 12 个 Verus/Rust 任务、四个模型家族、匹配调用预算下观察到这一“目标反转”。

在认证见证产率上，独立无反馈发现为 59.0%，高于 IntentShield 纠正性反馈循环的 27.1%，差距超过两倍。作者加入格式匹配的迭代对照，认为差距主要来自反馈内容本身，而非独立重启。该优势在每个模型家族都存在，并在解析器修复后仍然成立。

另一组分阶段执行在不复用响应的前提下达到相近总体产率；多数认证见证也未能通过留出用例。保留这些见证可改善规格修复：Phase-Revised 契约的实现成功率为 81.3%，IS-Revised 为 62.5%，Direct-Revised 略低。两种无反馈见证来源都明显优于被弱化的契约。

适用场景

面向使用 Verus/Rust 进行形式化规格审计、希望提升规格修复成功率的研究与工程实践。

限制与待核实

论文摘要明确说明：该效应在可获得的 Dafny 与 Lean 评估中没有复现，因此结论仅适用于所研究的 Verus/Rust 工作流。来源未给出任务细节、模型具体版本或复现材料，且该预印本未经同行评审，结论与数值均未经验证。