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

AI 摘要

该论文研究形式验证中的规格完整性审计问题，发现在Verus/Rust任务中，正确性反馈会抑制审计所需的证据。在12个任务、四个模型家族的对比实验中，无反馈独立发现策略的认证见证产出率为59.0%，远高于IntentShield纠正反馈循环的27.1%。作者提出先保留并认证被接受的错误程序、再进行修复的分阶段工作流，其修复后的规格实现成功率达81.3%，优于IS-Revised的62.5%。该效应在Dafny和Lean评估中未复现，表明结果特定于所研究的Verus/Rust工作流。

正文节选

When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus 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 IntentShi

发布时间：2026-10-17 12:00

抓取时间：2026-10-16 12:10

来源机构：arXiv