Source-linked AI summary
DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche
TL;DR
Generating Dafny verification annotations is difficult because manual annotation writing is tedious and existing LLM approaches can modify base logic or miss useful proof strategies. DafnyPro addresses these issues with diff-checking, invariant pruning, and hint augmentation, improving verification across four benchmarks. On DafnyBench, Claude 3.5 Sonnet with DafnyPro achieves 86% correct proofs, while fine-tuned smaller models achieve competitive results; the evaluation remains limited in foundation-model and fine-tuning coverage.
Problem
Manual Dafny annotation writing is tedious, while existing LLM approaches can alter base-code logic and fail to leverage effective proof strategies.
Method
DafnyPro combines parser-based diff-checking, verifier-guided pruning of unnecessary invariants, and retrieval of predefined problem-independent proof strategies.
Results
DafnyPro improves verification performance across four benchmarks; on DafnyBench, Claude 3.5 Sonnet achieves 86% correct proofs, a 16 percentage point improvement over prior state of the art.
Takeaways & Limitations
Fine-tuned 7B and 14B models integrated with DafnyPro provide competitive verification performance while maintaining computational efficiency.
Takeaways & Limitations
Foundation-model comparisons include only Claude 3.5/3.7 Sonnet, and fine-tuning experiments focus on supervised fine-tuning of Qwen models.
Abstract
from arXiv · showhide
We present DafnyPro, an inference-time framework that enhances LLMs for generating verification annotations in Dafny. DafnyPro comprises three key components: a diff-checker that prevents modifications to base program logic, a pruner that removes unnecessary invariants, and a hint-augmentation system that retrieves and applies predefined, problem-independent proof strategies. We evaluate DafnyPro using Claude Sonnet 3.5 and 3.7 on four benchmarks: Clover, MBPP-Dafny, HumanEval-Dafny, and DafnyBench, achieving consistent performance gains in all cases. Notably, on DafnyBench, the most challenging benchmark, Claude Sonnet 3.5 enhanced with DafnyPro achieves 86% correct proofs, a 16 pp improvement over the base model. We also fine-tune two Qwen models on training data derived from verification attempts by larger models enhanced with DafnyPro. Our 7B and 14B models achieve 68% and 70% correct proofs on DafnyBench, respectively, demonstrating that smaller models can maintain high verification accuracy.
1 Introduction
DafnyPro targets the difficulty and cost of manually generating Dafny verification annotations while addressing weaknesses in existing LLM-based approaches. It combines soundness checks, annotation refinement, proof-strategy retrieval, and strong benchmark results.
- Manual Dafny annotations such as loop invariants and ranking functions are tedious and require domain expertise.
- Existing iterative LLM approaches can alter base-code logic or fail to exploit effective proof strategies from related problems.
- DafnyPro uses parser-based diff-checking, verifier-guided annotation refinement, and retrieval of predefined problem-independent proof strategies.
- 86% correct proofs on DafnyBench with Claude 3.5 Sonnet represents a 16 percentage point improvement over prior state of the art.
- DafnyPro is presented alongside fine-tuned 7B and 14B models for efficiently deployable verification with competitive performance.
2 Related Work
Prior work improves formal verification through iterative verifier feedback and model adaptation, but the supplied related-work passages emphasize complementary inference-time and fine-tuning directions.
- Inference-time methods iteratively generate annotations, invoke the Dafny verifier, and use failed-attempt feedback to guide refinement.
- Clover and DafnyBench provide multi-turn verification procedures, while Laurel automatically generates missing assertions with LLMs.
- Dafny-Annotator uses supervised fine-tuning on DafnySynth, whereas PREFACE applies preference-based reinforcement learning using verifier reward signals.
3 Technical Contribution
DafnyPro addresses three technical problems in LLM-generated Dafny annotations: unsafe base-code changes, unnecessary invariant clauses, and missing structural proof hints.
- Preventing Code Modifications: Existing systems regenerate whole Dafny programs, making annotation generation easier but risking logic changes that compromise soundness.
- Preventing Code Modifications: The diff-checker strips annotations and verifies that regenerated code matches the original base code, providing a principled soundness check.
- Removing Unnecessary Clauses: Unnecessary invariant clauses can be non-inductive and waste feedback iterations, so DafnyPro introduces greedy invariant-clause pruning.
- Removing Unnecessary Clauses: The pruner removes non-inductive clauses, tests the remaining annotations against the post-condition, and restores the original version if pruning fails.
- Hint Augmentation: Generated invariants may still require problem-independent hints, such as assertions capturing structural properties of arrays.
- Hint Augmentation: DafnyPro retrieves relevant proof strategies and failed attempts during inference; eight strategies suffice to significantly improve performance.
4 DafnyPro
DafnyPro generates verified Dafny annotations through repeated LLM attempts that enforce unchanged base logic, prune non-inductive invariants, and incorporate proof hints. It evaluates this process across four benchmarks, with broad gains over the baseline and strong performance on DafnyBench.
- Algorithm: DafnyPro takes a base Dafny program, an annotation-generating LLM, fixed proof hints, and a maximum attempt count as inputs.The process seeks a verified annotated program or reports failure after the attempt limit.
- Algorithm: Each generated program passes a diff-checker before verification to ensure the original program logic is unchanged.The algorithm continues when the soundness check fails.
- Algorithm: Non-inductive invariant clauses are pruned, while relevant hints from each attempt are incorporated into subsequent generations.The verifier rechecks the program after pruning, and the process continues until success or the attempt limit.
- Evaluation: DafnyPro is evaluated on Clover, MBPP-Dafny, HumanEval-Dafny, and DafnyBench, whose task is generating annotations needed for verification.DafnyBench is the largest and most challenging dataset, containing 782 programs.
- Evaluation: The diff-checker fixed all 70 of 782 DafnyBench base programs with compilation errors caused by ad hoc annotation removal.This repair improved the percentage of verified programs.
- Evaluation: DafnyPro improved verification over the baseline by 5% on MBPP and 14–16% on the other three datasets for both Claude models.Both Claude Sonnet models with DafnyPro exceeded 85% on DafnyBench.
- Evaluation: Hint augmentation produced the largest improvements among the detailed DafnyPro components.Table 1b also reports gains from fixing the 70 DafnyBench programs.
5 Fine-Tuned Models for Efficient Deployment
DafnyPro supports efficient deployment by curating verifier-guided training data for smaller models and fine-tuning Qwen models. The resulting models improve verification performance, with complementary fine-tuning strategies combining effectively.
- Data Curation: DafnyPro uses larger models to curate high-quality training data because limited Dafny programs online hinder large-scale fine-tuning of smaller models.The data includes successful and failed verification attempts paired with verified annotations and informalized verifier errors.
- Fine-Tuning Setup: LoRA fine-tuning is applied to Qwen2.5-7B and Qwen3-14B, evaluated on 197 held-out DafnyBench programs with five DafnyPro attempts.The held-out programs and their generated attempts were excluded from fine-tuning.
- Results: A mixing strategy combining ground-truth and error-explanation fine-tuned models reaches a 69.5% verification rate after five attempts.The strategy uses the ground-truth model for the first three attempts and the error-explanation model for the final two.
6 Conclusion and Future Work
The paper concludes that DafnyPro improves verification accuracy through soundness checks, pruning, and proof-strategy hints, while identifying broader model evaluation and alternative fine-tuning as future directions.
- Conclusion: DafnyPro achieves state-of-the-art verification accuracy across multiple datasets, including DafnyBench.The framework combines diff-checking, pruning, and hint augmentation.
- Conclusion: The fine-tuned models provide competitive verification performance with computational efficiency.The paper presents these models as supporting practical formal reasoning systems powered by large language models.
- Future Work: Evaluation is limited because foundation-model comparisons include only Claude 3.5 and 3.7 Sonnet.The authors identify broader model evaluation as necessary to assess generalizability more comprehensively.
- Future Work: Future work may examine reinforcement learning-based fine-tuning and additional architectures to strengthen understanding of robustness and scalability.The current fine-tuning experiments focus on supervised fine-tuning of Qwen models.
A.1 Diff-Checker Details
The supplied appendix passages identify examples of model-induced base-code modification and a ground-truth solution.
- Diff-Checker Details: The appendix includes a ground-truth solution.
- Diff-Checker Details: Figure 8 presents examples of LLM-induced modifications in base code for cheating.The figure concerns modifications intended to pass verification without preserving the original logic.
- Diff-Checker Details: The supplied passages connect the appendix material to detecting or documenting changes to base code.
A.2 Pruning Details
The supplied appendix passages identify pruning as a way to remove unnecessary invariants and improve verification efficiency.
- Pruning Details: Pruning unnecessary invariants enables verification.
- Pruning Details: Pruning avoids wasted feedback iterations.
- Pruning Details: The appendix passage frames pruning as an efficiency-oriented verification intervention.
Tactic: Bridging Partial and Full Array Slices
Dafny verification benefits from explicit assertions that connect partial slice reasoning in loop invariants to complete-array representations in postconditions. Similar bridges expose relationships between intermediate sequences, recursive slice computations, and final array results.
- Tactic: Bridging Partial and Full Array Slices: Explicit assertions connect loop invariants over a[..i] with postconditions over a[..].After the loop, asserting a[..a.Length] == a[..] bridges the final loop state and the postcondition.
- Tactic: Bridging Partial and Full Array Slices: Assertions after array-building loops connect intermediate sequences with final array representations.The verifier may need an explicit equivalence between accumulated sequence data and the method’s returned array.
- Tactic: Bridging Partial and Full Array Slices: For recursive functions on slices, assertions can expose how consecutive slices grow and relate to the final postcondition.Inside the loop, assert arr[..i+1] == arr[..i] + [arr[i]]; after the loop, assert arr[..] == arr[..i].
- Tactic: Bridging Partial and Full Array Slices: Stronger global invariants can simplify slice-based membership reasoning when local invariants require complex case analysis.Removing redundant bounds and retaining invariants that directly support the postcondition can reduce verification difficulty.
- Tactic: Bridging Partial and Full Array Slices: Lexicographic decreases clauses handle recursive methods that normalize sign before reducing magnitude.A clause such as decreases x < 0, x represents progress in both the sign-normalization and numeric-descent phases.
- Tactic: Bridging Partial and Full Array Slices: Conditional invariants preserve verification when strict range conditions fail at loop entry or boundary inputs.The form edge_case || normal_case accommodates cases such as n = 0 or n = 1 while retaining stronger guarantees during ordinary execution.