AxDafny: Agentic Verified Code Generation in Dafny

“There is no comparison between the ease of adding unverified knowledge and the complexity of including a means for its autonomous verification.”

— Richard S. Sutton, Verification, Incomplete Ideas

Coding agents increasingly rely on an iterative generate–check–repair loop: a model proposes a solution, receives feedback from an environment, and refines its answer accordingly.

Formal methods provide a rich feedback signal: verifiers can identify specification violations, logical gaps in reasoning, and unhandled edge cases. This makes verified code generation a practical setting to study the effects of inference scaling in agentic coding. Despite this promise, applications of formal methods in mainstream AI tasks remain limited due to the specialized expertise they require.

In our ICML AI4Math Workshop paper, AxDafny: Agentic Verified Code Generation in Dafny, we study agentic code generation in Dafny. Dafny is a programming language with an additional verification layer: a Dafny method includes an implementation, a specification that states requirements on the inputs and guarantees on the outputs, and proof annotations that help an internal verifier check that the implementation satisfies the specification.

As an example, consider a Dafny function that sums the positive integers from 0 to n. We add a specification that requires the input n to be non-negative, and ensures that the returned sum is n(n+1)/2. The implementation uses a simple loop that increments an index i and adds it to the sum. To verify the implementation satisfies the specification, we add proof annotations: a loop invariant which states that at iteration i, the running sum s is equal to i(i+1)/2 and a final assertion that i = n. Together, these facts are sufficient to verify the implementation.

method Sum(n: int) returns (s: int)
  requires n >= 0
  ensures s == n * (n + 1) / 2
{
  var i := 0;
  s := 0;
  while i < n
    invariant 0 <= i <= n
    invariant s == i * (i + 1) / 2
  {
    i := i + 1;
    s := s + i;
  }
  assert i == n;
}

Dafny provides rich feedback when verification fails. It can pinpoint where a specification cannot be proven, identify missing termination arguments in loops or recursive methods, and can generate concrete counterexamples showing inputs that violate the specification. Once verified, Dafny programs can be compiled to standard programming languages such as Python, C#, or Java.

We introduce AxDafny, an agentic framework for program synthesis and proof synthesis that generates verified implementations through iterative verifier-guided repair. AxDafny builds on the AxProverBase architecture, which we described in an earlier blog post.

We evaluate AxDafny on two tasks:

• Proof synthesis: Given a valid implementation and specification, generate the proof annotations needed to verify that the implementation satisfies its specification.
• Program synthesis: Given a specification, generate the implementation and proof annotations needed to verify the implementation against the specification.

Proof synthesis

We evaluate AxDafny on DafnyBench, an established benchmark for proof synthesis using methods collected from public GitHub repositories. In DafnyBench, the original proof annotations are removed from each method, and the task is to restore enough proof annotations for verification. AxDafny verifies 725/782 instances (92.7%), outperforming the strongest previously reported proof-hint baseline by 6.5 percentage points.

Program synthesis

We introduce LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny), a new benchmark for evaluating program synthesis with formal specifications. This benchmark contains 250 problems, split into 100 easy, 100 medium, and 50 hard. LCB-Pro-Dafny is based on LiveCodeBench-Pro, a challenging state-of-the-art benchmark for evaluating AI code generation on competition-style programming tasks.

AxDafny performs strongly on LCB-Pro-Dafny, achieving a 56.4% success rate overall, nearly 5x the verification success rate of the GPT-5.5 pass@1 baseline. However, it verifies only 28.0% of problems in the hard split, showing that LCB-Pro-Dafny remains a challenging benchmark.

Finally, we test executable correctness by compiling verified Dafny outputs to Python and running the original LCB-Pro test harness. The harness evaluates each solution against unit tests under a fixed time limit for each problem. Among verified solutions, 32/75 easy problems, 6/52 medium problems, and 0/14 hard problems pass the executable tests. Most failures are due to runtime limits, such as time-limit exceeded (TLE) or memory-limit exceeded (MLE), showing that formal verification and executable performance measure different aspects of generated code.

We are releasing the code, benchmark datasets, and evaluation harness for LCB-Pro-Dafny, available here.