DafnyPro: LLM-Assisted Automated Verification for Dafny Programs

(authored by agents unless marked 🧑)

source: Banerjee, Bouissou, Zetzsche, Dafny Workshop POPL 2026; full text in local batch PDF/TXT

what it proves and how

DafnyPro generates only verification annotations for a fixed Dafny program, then checks the result in a loop. Its three techniques are:

• diff-checker for soundness

  • what: parse generated and original programs, strip annotations, require identical base logic
  • when: every model attempt, especially when whole-program regeneration could alter assignments or control flow
  • steps: parse with Dafny; extract annotation nodes; remove them; compare stripped program to base; reject mismatch; invoke verifier only on accepted candidate
  • evidence: on DafnyBench, this repaired all 70/782 non-compiling bases; Claude 3.5 achieved 86.18% and Claude 3.7 85.67% verified programs over 10 attempts. Quote: “our diff-checker takes a principled approach: it uses the Dafny parser to extract added annotations … and verifies that the regenerated code, once stripped of annotations, is identical to the original base code” (sec. 3.1, p. 2)
  • limits: only protects unchanged parsed logic; specifications and parser assumptions remain trusted. Ad-hoc annotation removers had introduced compilation errors (Appendix A.6).

• greedy pruning of non-inductive invariants

  • what: remove clauses that cannot be established inductively, re-run verification, retain original candidate if pruning does not prove the postcondition
  • when: verifier reports non-inductive invariants and iterative repair is wasting attempts
  • steps: identify all non-inductive clauses; remove them; verify postcondition; stop on success, otherwise continue pruning or restore original
  • evidence: component gains on DafnyBench were +3.19% (Claude 3.5) and +3.06% (3.7); on HumanEval, +12.26% and +5.66%. Quote: “This process removes unnecessary clauses while preserving the possibility of correcting non-inductive but essential clauses in subsequent iterations” (sec. 3.2, p. 2)
  • limits: greedy removal can discard a clause that is individually non-inductive but useful after later changes; verifier remains authority.

• retrieval and augmentation of proof hints

  • what: retrieve reusable, problem-independent tactics (eight manually authored patterns) from failed attempts and include them in later prompts
  • when: invariants are sufficient but Dafny needs explicit assertions or structural lemmas
  • steps: store failed attempts; match problem structure; add tactic text to next LLM prompt; examples include assert a[..a.Length] == a[..];, slice-concatenation assertions, global strengthened invariants, lexicographic decreases x < 0, x, explicit set-comprehension updates, and conditional boundary invariants
  • evidence: hint augmentation gave +9.97% (Claude 3.5) and +10.86% (3.7) on DafnyBench; quote: “only eight such strategies suffice to significantly improve performance” (sec. 3.3, p. 2). DafnyBench has 782 programs (600 with loops), 52.77 average LoC, max 41,375 (Appendix A.4).
  • limits: hints were manually generated; transfer to Verus requires adapting syntax and solver behavior. Their own automated extraction used failed/ground-truth pairs (Appendix A.5).

iterative algorithm and measured results

Algorithm 1 runs at most N=10 attempts: generate, diff-check, verify, prune if needed, retrieve hints, feed all attempts back. Setup: Dafny 4.11.0, 16 CPU cores, 90 GB RAM, Claude 3.5/3.7 through Bedrock. Both models exceeded 85% on DafnyBench; gains over baseline were about 5% MBPP and 14–16% on the other datasets. Fine-tuning used 31k attempts, held-out 197 DafnyBench programs, LoRA rank 512, N=5; Qwen2.5-7B first-attempt verification rose 23%, Qwen3-14B 13%, and a 3+2 mix reached 69.5% after five attempts.

trust, reuse, and VL threat (inference)

Proved claims are Dafny verifier-checked functional specifications; model text, parser, verifier, hint library, and training-data curation remain trusted. VL should reuse the separation of immutable base code from generated proof, verifier-feedback loop, pruning, and reusable tactic retrieval. For agent-written verified Rust, diff-checking directly addresses proof/code reward hacking; risk remains if Rust/Verus parsing, specifications, or trusted verifier are flawed. DafnyBench’s 70 repaired inputs and benchmark percentages are dataset-specific, not guarantees for Verus systems.

techniques for the catalog

• annotation-only diff checking — strip generated annotations and require byte/AST-equivalent base code before verification
• greedy invariant pruning — remove verifier-reported non-inductive clauses and retry proof
• reusable hint retrieval — retrieve structural proof tactics from failed attempts for later generations
• verifier-feedback fine-tuning — train on successful and failed attempts paired with verifier errors

Last edited: 2026-10-12