ProofPulse: Interactive Proof Coverage Analysis for Dafny

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.
Demo: https://www.youtube.com/watch?v=8pO3NAodjoQ
Code: https://github.com/VeriFixer/ProofPulse
Prebuilt Docker image: https://doi.org/10.5281/zenodo.21174686

Alexandra Mendes

Assistant Professor

My research focuses on encouraging a wider adoption of software verification by creating tools and methods that hide the complexities of verifying software. Much of my most recent work overlaps with the area of software engineering. For more details, see selected publications and some of my projects. Follow me on Twitter or add me on LinkedIn. See also the Software Reliability Lab website.