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