当正确性反馈消除反例：Verus 中的阶段分离式完备性审计

研究发现在 Verus/Rust 形式化验证任务中，传统的正确性反馈会抑制用于揭示规范不完备的反例程序。在 12 项任务与 4 个模型家族的测试中，无反馈的独立发现将认证反例生成率从 IntentShield 反馈循环的 27.1% 提升至 59.0% 以上。保留这些反例进行阶段分离式修复后，规范实现成功率达 81.3%，显著优于对比方案。