Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs

Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche

TL;DR

DafnyPro tackles the challenge of generating correct verification annotations for Dafny programs with LLMs, addressing soundness and efficiency. It introduces three mechanisms—diff-checking to prevent base-code modification, invariant pruning to remove unnecessary clauses, and hint augmentation to apply problem-independent proof strategies. The framework achieves state-of-the-art verification performance across multiple benchmarks, notably a strong result on DafnyBench, and demonstrates that smaller models can reach competitive accuracy through targeted data curation and fine-tuning. Together, these contributions enable practical, scalable, and robust LLM-assisted formal verification with tangible gains in accuracy and deployment efficiency.

Abstract

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.

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs

TL;DR

DafnyPro tackles the challenge of generating correct verification annotations for Dafny programs with LLMs, addressing soundness and efficiency. It introduces three mechanisms—diff-checking to prevent base-code modification, invariant pruning to remove unnecessary clauses, and hint augmentation to apply problem-independent proof strategies. The framework achieves state-of-the-art verification performance across multiple benchmarks, notably a strong result on DafnyBench, and demonstrates that smaller models can reach competitive accuracy through targeted data curation and fine-tuning. Together, these contributions enable practical, scalable, and robust LLM-assisted formal verification with tangible gains in accuracy and deployment efficiency.

Abstract

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.
Paper Structure (28 sections, 12 figures, 2 tables, 1 algorithm)

This paper contains 28 sections, 12 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Inference-time methods
  4. Model fine-tuning
  5. Technical Contribution
  6. Preventing Code Modifications
  7. Removing Unnecessary Clauses
  8. Incorporating Domain Knowledge
  9. DafnyPro
  10. Algorithm
  11. Evaluation
  12. Dataset Quality
  13. Setup
  14. Results
  15. Fine-Tuned Models for Efficient Deployment
  16. ...and 13 more sections

Figures (12)

  • Figure 1: Overview of the DafnyPro pipeline: (a) Merging, (b) Pruning, (c) Hint-Augmentation.
  • Figure 2: LLM modifies base code instead of only adding annotations, compromising soundness.
  • Figure 3: Pruning unnecessary invariants enables verification, avoiding wasted feedback iterations.
  • Figure 4: Problem-independent array slicing hint completes the proof.
  • Figure 5: DafnyPro performance with Claude 3.5 and 3.7 Sonnet.
  • ...and 7 more figures