# Dafny as Verification-Aware Intermediate Language for Code Generation

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 8 references that are in the map.
- First posted on arXiv 10 Jan 2025.

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

- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [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)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)

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

- [ProofWright: Towards Agentic Formal Verification of CUDA](https://mlsanity.com/paper/2511.12294/) (2025)
- [Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification](https://mlsanity.com/paper/2509.23061/) (2025)
- [Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning](https://mlsanity.com/paper/2509.06239/) (2025)
- [Containment Verification: AI Safety Guarantees Independent of Alignment](https://mlsanity.com/paper/2605.09045/) (2026)
- [Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python](https://mlsanity.com/paper/2607.03951/) (2026)
- [SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs](https://mlsanity.com/paper/2608.29841/) (2026)

## Abstract (arXiv)

Using large language models (LLMs) to generate source code from natural language prompts is a popular and promising idea with a wide range of applications. One of its limitations is that the generated code can be faulty at times, often in a subtle way, despite being presented to the user as correct. In this paper, we explore ways in which formal methods can assist with increasing the quality of code generated by an LLM. Instead of emitting code in a target language directly, we propose that the user guides the LLM to first generate an opaque intermediate representation, in the verification-aware language Dafny, that can be automatically validated for correctness against agreed on specifications. The correct Dafny program is then compiled to the target language and returned to the user. All user-system interactions throughout the procedure occur via natural language; Dafny code is never exposed. We describe our current prototype and report on its performance on the HumanEval Python code generation benchmarks.