{"ID":5443891,"CreatedAt":"2026-07-01T02:07:11.383974684Z","UpdatedAt":"2026-07-03T17:12:03.69683831Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2606.32007","arxiv_id":"2606.32007","title":"AxDafny: Agentic Verified Code Generation in Dafny","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.","short_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-...","url_abs":"https://arxiv.org/abs/2606.32007","url_pdf":"https://arxiv.org/pdf/2606.32007v1","authors":"[\"Benjamin Breen\",\"Austin Letson\",\"Borja Requena Pozo\",\"Leopoldo Sarra\"]","published":"2026-06-30T17:39:43Z","proceeding":"cs.AI","tasks":"[\"cs.AI\"]","methods":"[]","has_code":false}