AxDafny: Agentic Verified Code Generation in Dafny

Benjamin Breen, Austin Letson, Borja Requena Pozo, Leopoldo Sarra
6/30/2026
cs.AI

No confident code implementation found for this paper.

Abstract

We study agentic code generation in Dafny, where a model must generate both executable code and the proof artifacts for verification. We present AxDafny, a verifier-guided repair framework that iteratively generates implementations, invariants, assertions, and termination arguments. We also introduce LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny), a benchmark of 250 competition-style programming problems translated into Dafny with formal specifications and a verifier-based evaluation harness. On LCB-Pro-Dafny, AxDafny substantially improves verification success over baseline GPT-5.5 performance. On DafnyBench, AxDafny achieves 92.7\% verification success, outperforming the strongest previously reported proof-hint baseline by 6.5 percentage points. Lastly, we show that verification success and runtime test performance measure different aspects of generated code.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

From Verification Failures to Reusable Guidance for Coding Agents

87% match2026

PRO-V-R1: Reasoning Enhanced Programming Agent for RTL Verification

85% match1 repo362025

EDA-Aware RTL Generation with Large Language Models

85% match2024

FVSpec: Real-World Property-Based Tests as Lean Challenges

85% match2026

VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation

85% match2026

Automated Proof Generation for Rust Code via Self-Evolution

84% match2026

Cite this paper

@article{breen2026axdafny,
  title  = {AxDafny: Agentic Verified Code Generation in Dafny},
  author = {Benjamin Breen and Austin Letson and Borja Requena Pozo and Leopoldo Sarra},
  year   = {2026},
  eprint = {2606.32007},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2606.32007v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2606.32007.svg)](https://codeofpaper.com/paper/2606.32007)

Discussion