# From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 20 of its 75 references that are in the map.
- First posted on arXiv 24 Apr 2026.

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Gemma 3 Technical Report](https://mlsanity.com/paper/2503.19786/) (2025)
- [Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm](https://mlsanity.com/paper/2102.07350/) (2021)
- [SPoC: Search-based Pseudocode to Code](https://mlsanity.com/paper/1906.04908/) (2019)
- [Language Models of Code are Few-Shot Commonsense Learners](https://mlsanity.com/paper/2210.07128/) (2022)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [CWM: An Open-Weights LLM for Research on Code Generation with World Models](https://mlsanity.com/paper/2510.02387/) (2025)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Control the Temperature: Selective Sampling for Diverse and High-Quality LLM Outputs](https://mlsanity.com/paper/2510.01218/) (2025)
- [QED at Large: A Survey of Engineering of Formally Verified Software](https://mlsanity.com/paper/2003.06458/) (2020)
- [DafnyPro: LLM-Assisted Automated Verification for Dafny Programs](https://mlsanity.com/paper/2601.05385/) (2026)
- [Automating Code-Related Tasks Through Transformers: The Impact of Pre-training](https://mlsanity.com/paper/2302.04048/) (2023)
- [Concrete Semantics with Coq and CoqHammer](https://mlsanity.com/paper/1808.06413/) (2018)
- [More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme](https://mlsanity.com/paper/2205.00787/) (2022)
- [Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny](https://mlsanity.com/paper/2303.00152/) (2023)

## Abstract (arXiv)

Large Language Models (LLMs) show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code. To enforce model honesty, formal verification requires LLMs to synthesize implementation logic alongside formal specifications that are subsequently proven correct by a mathematical verifier. However, the transition from informal natural language to precise formal specification remains an arduous task. Our work addresses this by providing the NaturalLanguage2VerifiedCode (NL2VC)-60 dataset: a collection of 60 complex algorithmic problems. We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy: contextless prompts, signature prompts providing structural anchors, and self-healing prompts utilizing iterative feedback from the Dafny verifier. To address vacuous verification, where models satisfy verifiers with trivial specifications, we integrate the uDebug platform to ensure functional validation. Our results show that while contextless prompting leads to near-universal failure, structural signatures and iterative self-healing facilitate a dramatic performance turnaround. Specifically, Gemma 4-31B achieved a 90.91% verification success rate, while GPT-OSS 120B rose from zero to 81.82% success with signature-guided feedback. These findings indicate that formal verification is now attainable for open-weight LLMs, which serve as effective apprentices for synthesizing complex annotations and facilitating high-assurance software development.