AI 中文总结
ProofPulse是针对Dafny的交互式证明覆盖率分析工具，采用三值模型分析证明依赖，可诊断规范薄弱点，提升前置条件分类精准度，是验证的实用补充。
AI 中文摘要
演绎验证可确保实现满足其规范，但验证成功并不能保证规范的质量，因此薄弱的规范和冗余的不变量可能会让人对“已验证”的代码产生过度自信。我们提出了ProofPulse，一款针对Dafny的工具，它采用三值证明覆盖率模型来诊断规范质量。通过分析证明依赖关系，ProofPulse可区分出对规范意图有贡献的元素、仅用于辅助检查的元素，以及与任何证明义务无关的元素。针对来自dafny-synthesis基准的252个程序的参照标准进行评估，ProofPulse为规范薄弱点提供了高精准度的信号，尤其是不必要的前置条件和空泛证明。结合不可满足核心（unsat-core）最小化，ProofPulse实现了前置条件分类的完美精准度，并降低了所有评估类别中的误报率。这些结果表明，证明覆盖率是验证的实用补充，尽管它无法完全捕捉语义意图，但可以揭示原本看似已完全验证的程序中薄弱的证明耦合。就像脉搏检查能区分生命力与单纯没有症状一样，ProofPulse会暴露出那些技术上验证成功但仍存在代码或规范不足或冗余的证明中的薄弱点。
英文摘要
Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification. As such, weak specifications and redundant invariants may create overconfidence in ``verified'' code. We present \proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model. By analyzing proof dependencies, ProofPulse distinguishes between elements that contribute to specification intent, those used only for auxiliary checks, and those irrelevant to any proof obligation. Evaluated against an oracle of 252 programs from the dafny-synthesis benchmark, ProofPulse provides a high-precision signal for specification weaknesses, particularly unnecessary preconditions and vacuous proofs. With unsat-core minimization, ProofPulse achieves perfect precision for precondition classification and reduces false positives across all evaluated categories. These results show that proof coverage is a practical complement to verification. Although it cannot fully capture semantic intent, it can reveal weak proof coupling in programs that otherwise appear fully verified. Just as a pulse check distinguishes vitality from the mere absence of symptoms, ProofPulse exposes weaknesses in proofs that technically verify successfully but still suffer from inadequate or redundant code and specifications.
