mlsanityData to 7 Oct 2026

AxDafny: Agentic Verified Code Generation in Dafny

arXiv 2606.32007 ↗First posted 30 Jun 2026cs.AIcited by 1

On the map: LLM agents and tool use → Software engineering coding agents

Abstract (arXiv)

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.

Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use. Builds on 9 of its 12 references that are in the map. First posted on arXiv 30 Jun 2026.

Builds on

9 of 12 references.

Closest ancestors · 1

Same direction, newest first

  1. 2024SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering6 May

Other references · 8

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  2. 2021Program Synthesis with Large Language Modelscited by 3,509
  3. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  4. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  5. 2025LiveCodeBench Pro: How Do Olympiad Medalists Judge LLMs in Competitive Programming?cited by 52
  6. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  7. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Codecited by 7
  8. 2025Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verificationcited by 6

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 1.

1 paper.

  1. 2026VeriSkill: A Self-Evolution Framework for Program Verification Skillscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026P3: Joint Program-and-Proof Planning for Verified Code Generation
  2. 2026SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs
  3. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
  4. 2026SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
  5. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
  6. 2026Automating Formal Verification with Agent-Guided Tree Search
  7. 2026WybeCoder: Verified Imperative Code Generation
  8. 2026MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs