DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
summary
DafnyPro is an inference-time pipeline that uses LLMs (Claude Sonnet 3.5/3.7) to generate Dafny annotations while enforcing soundness with a diff-checker that rejects edits that change base program logic, a pruner that greedily removes non‑inductive invariants, and a hint-augmentation system that retrieves problem‑independent proof hints. Evaluated on Clover, MBPP‑Dafny, HumanEval‑Dafny and DafnyBench, it raises Claude Sonnet 3.5 on DafnyBench to 86% correct proofs (a 16 pp gain) and produces training data that yields Qwen 7B/14B models with 68%/70% success.
AI-written summary · about
chapters (15)
- 0:00DafnyPro introduction
- 1:51Generating Dafny annotations
- 3:18LLM annotation strategies
- 4:44Soundness risks in regeneration
- 5:47Formal check for logic
- 6:31Invariant generation cases
- 7:57Missing assertions and hints
- 9:25Verbose invariants pruning
- 10:48DafnyPro agentic framework
- 11:30Benchmark evaluation results
- 12:54Performance improvements
- 13:38Hint augmentation success
- 14:20Ensuring soundness
- 14:40Overthinking problem pruning
- 15:04Summary
related talks
23mdafny-annotator: AI-Assisted Verification of Dafny Programs
18mDafnyBench: A Benchmark for Formal Software Verification
15mDafny as Verification-Aware Intermediate Language for Code Generation
15mLaurel: Unblocking Automated Verification with Large Language Models
18mLaurel: Unblocking Automated Verification with Large Language Models
22mTowards Verified Code Reasoning by LLMs
21mVerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…)
01h 01mDiscussion