Sign up to save your podcasts
Or
Share Can LLMs Enable Mainstream Formal Verification?
Share to email
Share to Facebook
Share to X
Share to email
Share to Facebook
Share to X
Or
Can LLMs Enable Mainstream Formal Verification?
This episode explores whether large language models can help mainstream developers write code that is not just plausible, but formally verified in systems like Dafny, Nagini, and Verus. It explains the core ideas behind machine-checked correctness, including contracts, SMT solvers, loop invariants, and why verification is far stricter than passing tests or matching statistical behavior. The discussion highlights the paper’s main argument that the real bottleneck is not only generating implementations, but also generating the formal scaffolding and annotations that proofs require, especially around loops. Listeners get a clear view of how the authors evaluate LLMs with verifier feedback and extra validation to catch weakened specifications, making the episode interesting for anyone curious about whether AI can close the trust gap in code generation.
Sources:
1. Can LLMs Enable Verification in Mainstream Programming? — Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev, 2025
http://arxiv.org/abs/2503.14183
2. Inferring Loop Invariants using Postconditions — Carlo A. Furia, Bertrand Meyer, 2009
https://scholar.google.com/scholar?q=Inferring+Loop+Invariants+using+Postconditions
3. Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking — Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller, 2014
https://scholar.google.com/scholar?q=Inferring+Loop+Invariants+by+Mutation%2C+Dynamic+Analysis%2C+and+Static+Checking
4. LoopInvGen: A Loop Invariant Generator based on Precondition Inference — Saswat Padhi, Rahul Sharma, Todd Millstein, 2017
https://scholar.google.com/scholar?q=LoopInvGen%3A+A+Loop+Invariant+Generator+based+on+Precondition+Inference
5. On Scaling Data-Driven Loop Invariant Inference — Sahil Bhatia, Saswat Padhi, Nagarajan Natarajan, Rahul Sharma, Prateek Jain, 2019
https://scholar.google.com/scholar?q=On+Scaling+Data-Driven+Loop+Invariant+Inference
6. Dafny: An Automatic Program Verifier for Functional Correctness — K. Rustan M. Leino, 2010
https://scholar.google.com/scholar?q=Dafny%3A+An+Automatic+Program+Verifier+for+Functional+Correctness
7. Nagini: A Static Verifier for Python — Marco Eilers, Peter Muller, 2018
https://scholar.google.com/scholar?q=Nagini%3A+A+Static+Verifier+for+Python
8. Verus: Verifying Rust Programs using Linear Ghost Types (extended version) — Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel, 2023
https://scholar.google.com/scholar?q=Verus%3A+Verifying+Rust+Programs+using+Linear+Ghost+Types+%28extended+version%29
9. Can LLMs Enable Verification in Mainstream Programming? — Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev, 2025
https://scholar.google.com/scholar?q=Can+LLMs+Enable+Verification+in+Mainstream+Programming%3F
10. Clover: Closed-loop verifiable code generation — Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett, 2024
https://scholar.google.com/scholar?q=Clover%3A+Closed-loop+verifiable+code+generation
11. Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement — Pranjal Aggarwal, Bryan Parno, Sean Welleck, 2024
https://scholar.google.com/scholar?q=Alphaverus%3A+Bootstrapping+formally+verified+code+generation+through+self-improving+translation+and+treefinement
12. Can large language models transform natural language intent into formal method postconditions? — Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu K. Lahiri, 2024
https://scholar.google.com/scholar?q=Can+large+language+models+transform+natural+language+intent+into+formal+method+postconditions%3F
13. Laurel: Generating Dafny assertions using large language models — Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou, 2024
https://scholar.google.com/scholar?q=Laurel%3A+Generating+Dafny+assertions+using+large+language+models
14. Finding Inductive Loop Invariants using Large Language Models — Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma, 2023
https://scholar.google.com/scholar?q=Finding+Inductive+Loop+Invariants+using+Large+Language+Models
15. Towards Formal Verification of LLM-Generated Code from Natural Language Prompts — Aaron Councilman et al., 2025
https://arxiv.org/abs/2507.13290
16. Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification — Cheng Wen et al., 2024
https://arxiv.org/abs/2404.00762
17. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models — Lezhi Ma et al., 2024
https://arxiv.org/abs/2401.08807
18. Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? — Cedric Richter and Heike Wehrheim, 2025
https://arxiv.org/abs/2510.12702
19. Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors — Tianchi Li et al., 2026
https://arxiv.org/abs/2605.17914
20. Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers — Varun Bharti et al., 2025
https://arxiv.org/abs/2508.00419
21. LLM For Loop Invariant Generation and Fixing: How Far Are We? — Mostafijur Rahman Akhond et al., 2025
https://arxiv.org/abs/2511.06552
22. 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
23. AI Post Transformers: Generative File Systems: Replacing Code with Formal Specifications — Hal Turing & Dr. Ada Shannon, 2026
https://podcast.do-not-panic.com/episodes/2026-03-18-generative-file-systems-replacing-code-w-414029.mp3
24. 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: Can LLMs Enable Mainstream Formal Verification?
View all episodes
By mcgrofThis episode explores whether large language models can help mainstream developers write code that is not just plausible, but formally verified in systems like Dafny, Nagini, and Verus. It explains the core ideas behind machine-checked correctness, including contracts, SMT solvers, loop invariants, and why verification is far stricter than passing tests or matching statistical behavior. The discussion highlights the paper’s main argument that the real bottleneck is not only generating implementations, but also generating the formal scaffolding and annotations that proofs require, especially around loops. Listeners get a clear view of how the authors evaluate LLMs with verifier feedback and extra validation to catch weakened specifications, making the episode interesting for anyone curious about whether AI can close the trust gap in code generation.
Sources:
1. Can LLMs Enable Verification in Mainstream Programming? — Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev, 2025
http://arxiv.org/abs/2503.14183
2. Inferring Loop Invariants using Postconditions — Carlo A. Furia, Bertrand Meyer, 2009
https://scholar.google.com/scholar?q=Inferring+Loop+Invariants+using+Postconditions
3. Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking — Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller, 2014
https://scholar.google.com/scholar?q=Inferring+Loop+Invariants+by+Mutation%2C+Dynamic+Analysis%2C+and+Static+Checking
4. LoopInvGen: A Loop Invariant Generator based on Precondition Inference — Saswat Padhi, Rahul Sharma, Todd Millstein, 2017
https://scholar.google.com/scholar?q=LoopInvGen%3A+A+Loop+Invariant+Generator+based+on+Precondition+Inference
5. On Scaling Data-Driven Loop Invariant Inference — Sahil Bhatia, Saswat Padhi, Nagarajan Natarajan, Rahul Sharma, Prateek Jain, 2019
https://scholar.google.com/scholar?q=On+Scaling+Data-Driven+Loop+Invariant+Inference
6. Dafny: An Automatic Program Verifier for Functional Correctness — K. Rustan M. Leino, 2010
https://scholar.google.com/scholar?q=Dafny%3A+An+Automatic+Program+Verifier+for+Functional+Correctness
7. Nagini: A Static Verifier for Python — Marco Eilers, Peter Muller, 2018
https://scholar.google.com/scholar?q=Nagini%3A+A+Static+Verifier+for+Python
8. Verus: Verifying Rust Programs using Linear Ghost Types (extended version) — Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel, 2023
https://scholar.google.com/scholar?q=Verus%3A+Verifying+Rust+Programs+using+Linear+Ghost+Types+%28extended+version%29
9. Can LLMs Enable Verification in Mainstream Programming? — Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev, 2025
https://scholar.google.com/scholar?q=Can+LLMs+Enable+Verification+in+Mainstream+Programming%3F
10. Clover: Closed-loop verifiable code generation — Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett, 2024
https://scholar.google.com/scholar?q=Clover%3A+Closed-loop+verifiable+code+generation
11. Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement — Pranjal Aggarwal, Bryan Parno, Sean Welleck, 2024
https://scholar.google.com/scholar?q=Alphaverus%3A+Bootstrapping+formally+verified+code+generation+through+self-improving+translation+and+treefinement
12. Can large language models transform natural language intent into formal method postconditions? — Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu K. Lahiri, 2024
https://scholar.google.com/scholar?q=Can+large+language+models+transform+natural+language+intent+into+formal+method+postconditions%3F
13. Laurel: Generating Dafny assertions using large language models — Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou, 2024
https://scholar.google.com/scholar?q=Laurel%3A+Generating+Dafny+assertions+using+large+language+models
14. Finding Inductive Loop Invariants using Large Language Models — Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma, 2023
https://scholar.google.com/scholar?q=Finding+Inductive+Loop+Invariants+using+Large+Language+Models
15. Towards Formal Verification of LLM-Generated Code from Natural Language Prompts — Aaron Councilman et al., 2025
https://arxiv.org/abs/2507.13290
16. Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification — Cheng Wen et al., 2024
https://arxiv.org/abs/2404.00762
17. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models — Lezhi Ma et al., 2024
https://arxiv.org/abs/2401.08807
18. Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? — Cedric Richter and Heike Wehrheim, 2025
https://arxiv.org/abs/2510.12702
19. Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors — Tianchi Li et al., 2026
https://arxiv.org/abs/2605.17914
20. Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers — Varun Bharti et al., 2025
https://arxiv.org/abs/2508.00419
21. LLM For Loop Invariant Generation and Fixing: How Far Are We? — Mostafijur Rahman Akhond et al., 2025
https://arxiv.org/abs/2511.06552
22. 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
23. AI Post Transformers: Generative File Systems: Replacing Code with Formal Specifications — Hal Turing & Dr. Ada Shannon, 2026
https://podcast.do-not-panic.com/episodes/2026-03-18-generative-file-systems-replacing-code-w-414029.mp3
24. 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: Can LLMs Enable Mainstream Formal Verification?