ProofPulse: Interactive Proof Coverage Analysis for Dafny

• URL: http://arxiv.org/abs/2608.30818v1
• Date: Mon, 31 Aug 2026 14:00:31 GMT
• Title: ProofPulse: Interactive Proof Coverage Analysis for Dafny
• Abstract summary: Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification.<n>We present proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model.
• Score: 47.23158426199152
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• A distribution-free certification framework for trustworthy crash-severity prediction [1.089614199781423]
  We develop a certification layer that wraps any severity model unmodified.<n>On 5.2 million Texas records across seven base models spanning four decades, the layer attaches identical validity.<n>The framework is released as an open-source package with theorem-level tests.
  arXiv  Detail & Related papers  (2026-09-10T14:20:08Z)
• How Powerful are LLMs in Generating Formal Program Specifications? [20.791968710071973]
  Coins is an evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations.<n>We conduct a large scale study on HumanEval with a curated set of human written Rocq specifications.<n>Our results show that specification generation remains a formidable challenge, and that verification complexity can obscure genuine differences in specification quality.
  arXiv  Detail & Related papers  (2026-08-13T10:45:18Z)
• GoodDiffusion: Proactive Copyright Protection for Diffusion Bridge Models via Learnable Sample-specific Signatures [88.63093209858387]
  We propose GoodDiffusion, inspired by backdoor mechanisms, to enforce model-level use-time control.<n>GoodDiffusion preserves high-quality generation for authorized queries carrying valid signatures, yet refuses to generate for unauthorized inputs.<n>To strengthen security, we introduce a Learnable Signature Network (LSN) that assigns sample-specific signatures conditioned on each input.
  arXiv  Detail & Related papers  (2026-06-29T04:07:09Z)
• Decodable but Not Faithful: Coupling Natural-Language Rationales to Programmatic Verifiers [0.7212939068975618]
  Language models can generate plausible rationales for their predictions, but these explanations may not faithfully represent the model's internal reasoning.<n>We propose verifier-coupled reasoning, a framework that inserts inline claims into reasoning traces and trains an auxiliary consistency head to predict programmatic verifier outputs.<n>We find a gap between decodability and faithfulness: consistency training reliably makes verifier information decodable from rationale representations, but decodability does not guarantee faithful generation.
  arXiv  Detail & Related papers  (2026-06-19T18:37:24Z)
• Stress-Testing Neural Network Verifiers with Provably Robust Instances [10.017475431603389]
  We introduce a reusable framework for generating verification instances with ground-truth labels.<n>We also introduce the verification Difficulty Profile, a collection of estimable quantities capturing distinct sources of instance hardness.<n>Using our framework and these profiles, we evaluate five state-of-the-art verifiers and show that different instances stress distinct aspects of the verification pipeline.
  arXiv  Detail & Related papers  (2026-05-16T20:56:52Z)
• Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis [7.936959383169967]
  We present SpecRL, a reinforcement learning framework for specification in Dafny.<n>We use the fraction of negative tests rejected by a candidate specification as a signal of specification completeness.<n>Experiments show that SpecRL improves both specification strength and verification success over SFT and RL.
  arXiv  Detail & Related papers  (2026-04-07T12:53:42Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  We introduce ProofGrid, a benchmark suite for evaluating reasoning through machine-checkable proofs.<n>ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling.<n> Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts.
  arXiv  Detail & Related papers  (2026-04-07T01:19:41Z)
• COIN: Uncertainty-Guarding Selective Question Answering for Foundation Models with Provable Risk Guarantees [51.5976496056012]
  COIN is an uncertainty-guarding selection framework that calibrates statistically valid thresholds to filter a single generated answer per question.<n>COIN estimates the empirical error rate on a calibration set and applies confidence interval methods to establish a high-probability upper bound on the true error rate.<n>We demonstrate COIN's robustness in risk control, strong test-time power in retaining admissible answers, and predictive efficiency under limited calibration data.
  arXiv  Detail & Related papers  (2025-06-25T07:04:49Z)
• CertDW: Towards Certified Dataset Ownership Verification via Conformal Prediction [48.82467166657901]
  We propose the first certified dataset watermark (i.e., CertDW) and CertDW-based certified dataset ownership verification method.<n>Inspired by conformal prediction, we introduce two statistical measures, including principal probability (PP) and watermark robustness (WR)<n>We prove there exists a provable lower bound between PP and WR, enabling ownership verification when a suspicious model's WR value significantly exceeds the PP values of benign models trained on watermark-free datasets.
  arXiv  Detail & Related papers  (2025-06-16T07:17:23Z)
• TrustLoRA: Low-Rank Adaptation for Failure Detection under Out-of-distribution Data [62.22804234013273]
  We propose a simple failure detection framework to unify and facilitate classification with rejection under both covariate and semantic shifts.<n>Our key insight is that by separating and consolidating failure-specific reliability knowledge with low-rank adapters, we can enhance the failure detection ability effectively and flexibly.
  arXiv  Detail & Related papers  (2025-04-20T09:20:55Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
  We present AmbiFC, a fact-checking dataset with 10k claims derived from real-world information needs. We analyze disagreements arising from ambiguity when comparing claims against evidence in AmbiFC. We develop models for predicting veracity handling this ambiguity via soft labels.
  arXiv  Detail & Related papers  (2021-04-01T17:40:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.