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 D
Lineage graph
Paper → model → repo connections mined from source citations (Tier-1 exact match).
Why these links exist
Every edge carries a method, confidence, and the source snippet that justified it — so bad links are debuggable.
- LinkedLinked via unknownScarfBench: Benchmarking AI Agents for Enterprise Java Framework Migration →
- PossiblePossibly related (embedding) · 55%Dryxio/auto-re-agent →
- FuzzySimilar title/name (fuzzy) · 59%Fosowl/agenticSeek →
“Fuzzy title match (0.73): “AxDafny: Agentic Verified Code Generation in Dafny” ≈ “Fosowl/agenticSeek””