dafny-annotator: AI-Assisted Verification of Dafny Programs
summary
Built a tool called dafny-annotator that uses LLMs plus greedy search (five iterations, five candidates) to insert invariants, decreases, and assertions into Dafny methods until Z3 verifies them. Base LLaMa 3.1 8B and Code Llama 7B verify ~15.7% and ~40% of held-out DafnyBench methods; after fine-tuning on real+synthetic data (the DafnySynth pipeline generated with GPT‑4o and filtered by Dafny) LLaMa 8B reaches 50.6%. The pipeline costs about $10 of OpenAI API credit to match DafnyBench scale.
AI-written summary · about
chapters (13)
- 0:00Dafny-Annotator intro
- 1:07Why formal verification unused
- 2:30Z3’s correct but unconvinced code
- 3:33Auto-adding Dafny annotations
- 5:16Small LLMs on Dafny bench
- 7:45Fine-tuning with little data
- 9:52Defin-Synth for synthetic Dafny
- 11:36Defin-Synth pipeline design
- 13:19Priority queue example
- 14:49Synthetic data results
- 15:31AI verification potential
- 16:36Summary and future work
- 16:57Q&A
related talks
16mDafnyPro: LLM-Assisted Automated Verification for Dafny Programs
15mLaurel: Unblocking Automated Verification with Large Language Models
18mSpecification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
20mCLOVER: Closed-Loop Verifiable Code Generation
22mTowards Verified Code Reasoning by LLMs
53mSemantics-based program manipulation in the age of LLMs
43mAI Development Lifecycle: Learnings of What Changed with LLMs
16mLemur: Integrating Large Language Models in Automated Program Verification