AxDafny: Agentic Verified Code Generation in Dafny

Source

• Source name: arXiv
• Source kind: paper
• Authors / organization: Benjamin Breen, Austin Letson, Borja Requena Pozo, Leopoldo Sarra
• Venue: arXiv: cs.AI
• Published: 2026-06-30
• Collected: 2026-07-01
• URL: http://arxiv.org/abs/2606.32007v1
• PDF: https://arxiv.org/pdf/2606.32007v1
• DOI: UNKNOWN

Plain-Language Brief

Researchers present AxDafny, a framework for generating executable code and proof artifacts in Dafny using a verifier-guided repair method. The study uses a benchmark called LiveCodeBench-Pro-Dafny with 250 programming problems and shows that AxDafny improves verification success over GPT-5.5 on this benchmark, achieving 92.7% verification success on DafnyBench.

What the Document Says

• The study is about agentic code generation in Dafny.
• AxDafny is a verifier-guided repair framework for generating implementations, invariants, assertions, and termination arguments in Dafny.
• LiveCodeBench-Pro-Dafny is a benchmark of 250 competition-style programming problems translated into Dafny with formal specifications and a verifier-based evaluation harness.
• On LiveCodeBench-Pro-Dafny, AxDafny improves verification success over GPT-5.5.
• AxDafny achieves 92.7% verification success on DafnyBench.
• AxDafny outperforms the strongest previously reported proof-hint baseline by 6.5 percentage points on DafnyBench.

Key Concepts Mentioned

• code generation
• Dafny
• verifier-guided repair
• LiveCodeBench-Pro-Dafny
• GPT-5.5
• verification success
• DafnyBench

Claims Made by the Document

• AxDafny improves verification success over GPT-5.5 on LiveCodeBench-Pro-Dafny.
• AxDafny achieves higher verification success than the strongest previously reported proof-hint baseline on DafnyBench.

Evidence Used

• The study shows that AxDafny substantially improves verification success over GPT-5.5 performance on LiveCodeBench-Pro-Dafny.
• On DafnyBench, AxDafny achieves 92.7% verification success.

Methods / Approach

• Verifier-guided repair framework
• Use of benchmarks for evaluation

Limitations Stated by the Authors

UNKNOWN

Limitations Noted by the Agent

Agent interpretation — not from the source.

UNKNOWN

Open Questions

UNKNOWN

Notes for Future Q&A

May include interpretation. Labeled where it does.

UNKNOWN

Raw Abstract / Excerpt

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.