AxDafny: Agentic Verified Code Generation in Dafny

(authored by agents unless marked 🧑)

scope and prior notes

This study covers Breen et al.’s AxDafny paper (arXiv:2606.32007, 2026) from the complete extracted text, including appendices. I found no earlier note with this exact title in /ssd1/sichanghe.github.io/src/notes/research/; therefore this is new coverage.

what is proved and what remains trusted

AxDafny asks an agent to synthesize both executable Dafny and proof annotations, then uses Dafny’s SMT verifier as feedback. A candidate is accepted only when the fixed specification is preserved, no proof-bypass syntax appears, Dafny verifies, and an LLM reviewer finds no cheating. The paper says, “A candidate is accepted only if it passes the preservation checks, contains no rejected proof-bypass constructs, verifies with Dafny, and is not rejected by the LLM reviewer.” (section 3.1, page 3). The method proves properties expressed by requires/ensures, loop invariants, assertions, and termination obligations under Dafny’s verifier. The specification itself, Dafny implementation of the verifier, compiler/runtime, benchmark tests, and the LLM review remain trusted. The authors explicitly caution that “our evaluation therefore treats the specification as a trusted object and explicitly checks for specification modification and vacuous proof shortcuts.” (discussion, page 6). Thus verification does not establish that the specification matches user intent or resource bounds.

technique 1: verifier-guided generate–review–repair

What it is: an iterative proposer/reviewer/memory architecture. When to use it: when code and proof hints must be synthesized jointly and a sound verifier can provide actionable diagnostics. How to apply:

1. Give a proposer the original Dafny file, target name, and previous memory; require a complete annotated file while preserving original requires and ensures.
2. Run deterministic preservation checks by extracting clauses from original and candidate and requiring the originals to be a subset of candidate clauses.
3. Reject regex matches for {:axiom}, {:verify false}, assume, and {:extern}; return offending lines.
4. Run dafny verify; feed unmet preconditions, postconditions, invariants, termination checks, source locations, and optional concrete counterexamples back to the proposer.
5. Ask an LLM reviewer to detect semantic cheating such as rewriting a predicate to true; accept only after this review.
6. Maintain both the previous attempt verbatim and an LLM-generated rolling scratchpad across iterations.

The paper’s exact architecture description is: “The proposer writes Dafny code, the review system checks it and returns concrete feedback, and the memory module preserves information across iterations.” (section 3.1, page 3). A practical code shape is the paper’s Sum method: requires n >= 0, ensures s == n * (n + 1) / 2, loop invariants 0 <= i <= n and s == i * (i + 1) / 2, and a final assert i == n (Figure 1, page 2). The fixed evaluation budget was 20 attempts per instance (section 3.2, page 3).

Evidence: on DafnyBench, Gemini-3.1-Pro AxDafny verified 725/782 instances (92.7%); GPT-5.5 medium verified 695/782 (88.9%) and low 85.3%. The 92.7% result is 6.5 percentage points above DafnyPro’s 86.2% (which uses retrieval) and 16.5 points above DafnyPro without hints (76.2%). On LCB-Pro-Dafny, AxDafny verified 75/100 easy, 52/100 medium, and 14/50 hard, overall 141/250 (56.4%), versus direct GPT-5.5 pass@1 at 13/100, 14/100, and 2/50 (29/250, 11.6%). Gains continue through 15 iterations, while proof-hint gains concentrate in the first five (Figure 2/3, pages 4–5).

Limits: hard end-to-end synthesis reaches only 28.0%. The verifier checks functional specifications, generally not asymptotic complexity or memory, and verified outputs often fail runtime limits: among easy verified outputs, 32/75 pass tests, 39/75 TLE, 4/75 MLE; medium, 6/52 pass, 44/52 TLE, 2/52 MLE (section 4, page 5). Dafny-to-Python runtime implementations can also be slow. Benchmark specifications required curation: LLM review flagged 14/250 (5.6%) for semantic fixes, all revised (section 3.3 and Appendix A, pages 3, 7).

technique 2: benchmark and acceptance harness for verified synthesis

What it is: LCB-Pro-Dafny translates 250 competition problems (100 easy, 100 medium, 50 hard) into tasks containing a natural-language statement, Dafny signature, and formal specification. Use it to measure joint program/proof synthesis separately from executable performance. The harness first requires Dafny verification, unchanged provided definitions/specifications, and no assume/{:extern} shortcuts; only verified files are compiled to Python and run against original tests. The paper states, “A solution is accepted only when (1) the generated implementation verifies in Dafny, (2) the provided specification, definitions, and functions are not modified, and (3) the solution does not rely on vacuous proof shortcuts.” (section 3.4, page 3). Evidence and denominators are the 56.4% (141/250) verifier rate above; secondary tests expose resource failures among verified outputs. Appendix A reports all 250 parse/type-resolve under Dafny 4.11.0, 14/250 semantic mismatches fixed, and no placeholder implementation verified in 234 mutation-harness cases. Assumptions/failures: specification quality is a curation bottleneck; runtime-test success and formal verification measure different properties and are not directly comparable.

implications for verified Rust and VL (inference)

The architecture is a strong analog for agent-written verified Rust: preserve user contracts, reject bypasses, invoke a machine checker, feed diagnostics into bounded repair, and retain attempt memory. However, Dafny’s integrated verifier and simpler memory model remove unsafe aliasing and borrow-checker interactions; Rust would need separate tools for safe and unsafe code and explicit resource specifications. The 56.4% end-to-end rate and hard-split 28.0% indicate substantial product risk if “verified” is presented as runtime-efficient or specification-correct. The paper’s own trust statement means VL must review specifications and compiler/toolchain assumptions, not only checker acceptance. Existing work VL should not redo: a verifier-guided loop, clause-preservation checks, anti-vacuity filters, counterexample feedback, and separate verification/runtime metrics are already demonstrated here.

techniques for the catalog

• verifier-guided repair loop — generate complete annotated code, run preservation/anti-bypass checks and Dafny, then repair from diagnostics with bounded memory
• contract-preservation filter — require original requires/ensures to remain a subset of the candidate
• anti-bypass static and LLM review — reject assume, {:axiom}, {:verify false}, {:extern}, and semantic tautologies
• counterexample feedback — enable Dafny counterexamples to expose invalid proof obligations concretely
• dual verification/runtime evaluation — report machine verification and compiled test performance as separate metrics
• curated verified-code benchmark — validate fixed specifications with parsing, type resolution, mutation, LLM, and manual checks before use

Last edited: 2026-10-12