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

The paper presents AxDafny, a framework for generating executable code and verification artifacts in Dafny using a verifier-guided repair approach. The framework significantly improves verification success over the baseline GPT-5.5 performance on a benchmark of programming problems called LiveCodeBench-Pro-Dafny. AxDafny achieves 92.7% verification success on DafnyBench, outperforming the strongest previously reported proof-hint baseline by 6.5 percentage points.

What the Document Says

• The study focuses on agentic code generation in Dafny.
• AxDafny is presented as a verifier-guided repair framework that iteratively generates implementations, invariants, assertions, and termination arguments.
• LiveCodeBench-Pro-Dafny, a benchmark of 250 competition-style programming problems translated into Dafny with formal specifications and a verifier-based evaluation harness, is introduced.
• On LiveCodeBench-Pro-Dafny, AxDafny substantially improves verification success over baseline GPT-5.5 performance.
• On DafnyBench, AxDafny achieves 92.7% verification success and outperforms the strongest previously reported proof-hint baseline by 6.5 percentage points.
• It is mentioned that verification success and runtime test performance measure different aspects of generated code.

Key Concepts Mentioned

• Agentic code generation
• Dafny
• AxDafny
• LiveCodeBench-Pro-Dafny
• verification success
• GPT-5.5

Claims Made by the Document

• AxDafny substantially improves verification success over GPT-5.5 on LiveCodeBench-Pro-Dafny.
• AxDafny outperforms the strongest previously reported proof-hint baseline on DafnyBench by 6.5 percentage points.

Evidence Used

• Improvement in verification success on LiveCodeBench-Pro-Dafny compared to GPT-5.5.
• Achieving 92.7% verification success on DafnyBench and outperforming the strongest previously reported proof-hint baseline.

Methods / Approach

UNKNOWN

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.