# Can LLMs Enable Verification in Mainstream Programming?

arXiv: https://arxiv.org/abs/2503.14183 · HTML: https://mlsanity.com/paper/2503.14183/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 33 references that are in the map.
- First posted on arXiv 18 Mar 2025.

## Builds on (most cited first, 15 of 15)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://mlsanity.com/paper/2405.01787/) (2024)
- [Leveraging Large Language Models for Automated Proof Synthesis in Rust](https://mlsanity.com/paper/2311.03739/) (2023)
- [dafny-annotator: AI-Assisted Verification of Dafny Programs](https://mlsanity.com/paper/2411.15143/) (2024)
- [SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic](https://mlsanity.com/paper/1903.09713/) (2019)
- [Leveraging Large Language Models to Boost Dafny's Developers Productivity](https://mlsanity.com/paper/2401.00963/) (2024)
- [Formal Verification of the Ethereum 2.0 Beacon Chain](https://mlsanity.com/paper/2110.12909/) (2021)
- [Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)](https://mlsanity.com/paper/2407.09143/) (2024)

## Built on by (most cited first, 3 of 3)

- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [ExVerus: Verus Proof Repair via Counterexample Reasoning](https://mlsanity.com/paper/2603.25810/) (2026)

## Abstract (arXiv)

Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-ofthe-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results.