ProofPulse: Interactive Proof Coverage Analysis for Dafny
2026-08-31 • Software Engineering
Software Engineering
AI summaryⓘ
The authors created ProofPulse, a tool that helps check how good program specifications are after a verification process. Even if a program passes verification, its specifications might still be weak or have unnecessary parts. ProofPulse looks at which parts of the specification actually help prove the program correct and which parts don't. By testing many programs, the authors showed that ProofPulse can accurately find weak points like useless conditions or proofs that don’t really check anything. This tool helps programmers trust that their verified code is truly well specified, not just technically correct.
deductive verificationDafnyproof coveragespecification qualityinvariantspreconditionsunsat-core minimizationvacuous proofsproof dependenciesoracle benchmark
Authors
Álvaro F. Silva, Ruben Martins, Alexandra Mendes
Abstract
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.