DafnyPro for LLM-Assisted Dafny Verification

This episode explores DafnyPro, a system for using large language models to help verify Dafny programs while keeping the original executable logic unchanged. It explains the basics of formal verification in Dafny, including preconditions, postconditions, loop invariants, decreases clauses, ghost code, and why writing correct proof annotations is much harder than generating plausible code. The discussion compares DafnyPro with earlier efforts such as Clover, DafnyBench, and Laurel, then focuses on DafnyPro’s main contribution: a parser-backed safeguard that rejects any LLM attempt that alters program behavior and a verifier-guided loop that can also prune bad invariants instead of blindly adding more. A listener would find it interesting because it gets at a real trust problem in AI coding tools: whether a model can genuinely help prove software correct rather than quietly rewriting the task into something easier to verify. Sources: 1. DafnyPro: LLM-Assisted Automated Verification for Dafny Programs — Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche, 2026 http://arxiv.org/abs/2601.05385 2. Clover: Closed-Loop Verifiable Code Generation — Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett, 2023 https://arxiv.org/abs/2310.17807 3. DafnyBench: A Benchmark for Formal Software Verification — Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark, 2024 https://arxiv.org/abs/2406.08467 4. Laurel: Unblocking Automated Verification with Large Language Models — Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou, 2024 (rev. 2025) https://arxiv.org/abs/2405.16792 5. DafnyPro: LLM-Assisted Automated Verification for Dafny Programs — Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche, 2026 https://arxiv.org/abs/2601.05385 6. Laurel: Generating Dafny Assertions Using Large Language Models — Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou, 2024 https://arxiv.org/abs/2405.16792 7. dafny-annotator: AI-Assisted Verification of Dafny Programs — Gabriel Poesia, Chloe Loughridge, Nada Amin, 2024 https://arxiv.org/abs/2411.15143 8. Towards AI-Assisted Synthesis of Verified Dafny Methods — Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, James Noble, 2024 https://arxiv.org/abs/2402.00247 9. Inferring multiple helper Dafny assertions with LLMs — Alvaro Silva, Alexandra Mendes, Ruben Martins, 2025 https://arxiv.org/abs/2511.00125 10. Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification — Kyle Thompson et al., 2024 https://scholar.google.com/scholar?q=Rango%3A+Adaptive+Retrieval-Augmented+Proving+for+Automated+Software+Verification 11. Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming — Saikat Chakraborty et al., 2024 https://scholar.google.com/scholar?q=Towards+Neural+Synthesis+for+SMT-Assisted+Proof-Oriented+Programming 12. Finding Inductive Loop Invariants using Large Language Models — Adharsh Kamath et al., 2023 https://scholar.google.com/scholar?q=Finding+Inductive+Loop+Invariants+using+Large+Language+Models 13. A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification — Norbert Tihanyi et al., 2023 https://scholar.google.com/scholar?q=A+New+Era+in+Software+Security%3A+Towards+Self-Healing+Software+via+Large+Language+Models+and+Formal+Verification 14. Rethinking Optimal Verification Granularity for Compute-Efficient Test-Time Scaling — Hao Mark Chen et al., 2025 https://scholar.google.com/scholar?q=Rethinking+Optimal+Verification+Granularity+for+Compute-Efficient+Test-Time+Scaling 15. Heimdall: test-time scaling on the generative verification — Wenlei Shi and Xing Jin, 2025 https://scholar.google.com/scholar?q=Heimdall%3A+test-time+scaling+on+the+generative+verification 16. AI Post Transformers: From Natural Language to Verified Dafny Code — Hal Turing & Dr. Ada Shannon, 2026 https://podcast.do-not-panic.com/episodes/2026-06-14-from-natural-language-to-verified-dafny-8abed9.mp3 17. AI Post Transformers: DeepVerifier: Self-Evolving Research Agents via Rubric-Guided Verification — Hal Turing & Dr. Ada Shannon, 2026 https://podcast.do-not-panic.com/episodes/deepverifier-self-evolving-research-agents-via-rubric-guided-verification/ 18. AI Post Transformers: Agentic Discovery for Test-Time Scaling — Hal Turing & Dr. Ada Shannon, 2026 https://podcast.do-not-panic.com/episodes/2026-05-12-agentic-discovery-for-test-time-scaling-f9a81f.mp3 19. AI Post Transformers: Trajectory Summaries for Long-Horizon Coding Agents — Hal Turing & Dr. Ada Shannon, 2026 https://podcast.do-not-panic.com/episodes/2026-05-24-trajectory-summaries-for-long-horizon-co-0194be.mp3 Interactive Visualization: DafnyPro for LLM-Assisted Dafny Verification