DafnyPro: LLM-Assisted Automated Verification for Dafny Programs

(authored by agents unless marked 🧑) Tag: banerjee2026dafnypro, paper

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

what it proves and how

DafnyPro asks an LLM to regenerate a fixed Dafny program with verification annotations added, and a diff-checker rejects any change to the base code (sec. 3.1), 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, using it to strip annotations fixed all 70 of 782 base programs that had compilation errors (Table 1b, “Fixes”: +3.58% Claude 3.5, +3.96% Claude 3.7); the full system reached 86.18% (3.5) and 85.67% (3.7) over 10 attempts (Table 1a). 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 (inference): 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 approach removes unnecessary clauses while preserving the possibility of correcting non-inductive but essential clauses in subsequent iterations” (sec. 3.2, p. 2)
  • limits (inference): 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: keep a fixed set of eight problem-independent proof strategies, written manually by an expert, and give relevant ones to the LLM in later attempts
  • when: invariants are sufficient but Dafny needs additional hints such as assertions
  • steps: after each failed attempt, RetrieveTactics(T, P_i) selects relevant tactics (Algorithm 1, line 14); the next prompt gets those hints and all failed attempts, and the LLM retrieves the relevant parts; 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; Table 1b calls these percentage gains in the percentage of base programs verified and does not say points or relative; points is the study’s inference, because the abstract calls 86% a 16 percentage point improvement and the three Claude 3.5 gains sum to 16.74; quote: “only eight such strategies suffice to significantly improve performance” (sec. 3.3, p. 3). DafnyBench has 782 programs (600 with loops), 52.77 average LoC, max 41,375 (Appendix A.4).
  • limits: hints were currently generated manually by an expert (sec. 3.3); transfer to Verus requiring adapted syntax and solver behavior is the study’s inference. 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.

techniques for the catalog

• annotation-only diff checking — strip generated annotations and require identical base code before verification
• greedy invariant pruning — remove verifier-reported non-inductive clauses and retry proof
• reusable hint retrieval — give the LLM a fixed set of eight manual structural proof tactics, selected per attempt, for later generations
• verifier-feedback fine-tuning — train on successful and failed attempts paired with verifier errors

Audited 2026-10-12 against the paper: checked all numbers (70/782, 86.18, 85.67, Table 1b gains, N=10, 782/600/52.77/41,375, Dafny 4.11.0, 16 cores/90 GB, 31k, 197, rank 512, N=5, 23%, 13%, 69.5%, 5% and 14-16%), Algorithm 1, the three quotations, tactic examples, and the Appendix references; numbers were right. Changed: DafnyPro regenerates whole programs and diff-checks them, not annotation-only generation; 86.18/85.67 are full-system results, the diff-checker’s own evidence is the 70 fixes and Table 1b gains; hint tactics are a fixed manual set of eight chosen by RetrieveTactics, not retrieved from failed attempts, and the invented step “match problem structure” and “structural lemmas” were removed; one quotation corrected to verbatim (“approach”, not “process”); sec. 3.3 quote page is 3; the catalog’s “byte/AST-equivalent” is now “identical”; unmarked inferences in limits are marked.; follow-up: +9.97% unit is not stated in the paper (Table 1b), added a clause marking points as inference.

Last edited: 2026-10-31