AxDafny: Agentic Verified Code Generation in Dafny

Benjamin Breen ,

Austin Letson ,

Borja Requena Pozo ,

Leopoldo Sarra

LLM CoT Other LLM Agent Agent Planning Tool Learning AI Systems and Hardware PVDAR Text-to-Code

我们研究了在 Dafny 语言环境下的“具身式”代码生成任务，即模型需同时生成可执行代码及其配套的形式化验证辅助构件（如证明脚手架）。为此，我们提出了 AxDafny——一种由验证器驱动的迭代修复框架，该框架能够循环生成程序实现、不变式、断言以及终止性论证。此外，我们构建了 LiveCodeBench-Pro-Dafny（LCB-Pro-Dafny）基准测试集：它包含 250 道面向竞赛风格的编程题目，全部被严谨地翻译为 Dafny 语言，并配有形式化规约及基于验证器的自动化评估框架。在 LCB-Pro-Dafny 上，AxDafny 在验证通过率上显著超越了基线模型 GPT-5.5 的表现；在 DafnyBench 基准上，AxDafny 实现了 92.7% 的验证通过率，较此前报道的最佳“证明提示”（proof-hint）基线方法提升了 6.5 个百分点。最后，我们证实：验证通过率与运行时测试准确率衡量的是生成代码的两个不同维度——前者反映代码在形式化逻辑层面的正确性，后者则体现其在具体输入输出行为上的功能性表现。

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.

许愿