想搞形式化验证代码生成？这篇论文的 AxDafny 用验证器做迭代修复，把 Dafny 编程题的验证成功拉到 92.7%，比之前的最好方法还高 6.5 个百分点。
AxDafny 是一种基于验证器引导的修复框架，可迭代生成实现、不变式、断言和终止参数。研究者引入了 LCB-Pro-Dafny 基准，包含 250 道竞赛编程题，配有形式化规范和验证评估。在 LCB-Pro-Dafny 上，AxDafny 相比 GPT-5.5 基线显著提升验证成功率。在 DafnyBench 上，AxDafny 达到 92.7% 验证成功率，比此前最强的证明提示基线高出 6.5 个百分点。实验还表明，验证成功与运行时测试表现衡量了代码生成的不同方面。
AxDafny: Agentic Verified Code Generation in Dafny
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.