Proving Instead of Testing

What formal verification means for code that AI writes

Something has shifted in how software comes into existence. A growing share of the code running in production was never typed line by line by a human — it was generated by a coding agent. That scales beautifully, right up to the moment you ask yourself who is actually still reviewing all of it.

A recent paper from researchers at UW-Madison and Princeton, MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs, tackles exactly that problem. Not with better tests, but with a mathematical proof. The idea is worth sitting with for a while, even if you never touch formal methods yourself.

The problem: testing proves nothing

The usual tools for checking generated code — fuzz testing, static analysis, and these days “LLM-as-a-Verifier,” where one language model reviews another’s output — catch plenty of bugs. But they share a structural limitation: they all look at a sample.

A test runs your code with concrete input and checks whether the answer is right. That proves something about that input. Fuzzing does the same thing, just with a lot more random values. Neither says anything about the cases you didn’t try. As Dijkstra put it back in 1970: testing can demonstrate the presence of bugs, never their absence.

For most software that’s an acceptable trade-off. For a CUDA kernel where thousands of threads write to memory in parallel, or for the control loop of a robotic arm, it becomes a different story. There, the edge case you didn’t test is precisely the one that takes you down.

The other route: a proof

Formal verification inverts the question. Instead of “does it work for this input?” you ask: can I prove it works for every possible input? — without ever running the code.

That sounds ambitious, but it’s exactly what a mathematical proof does. If you prove that the sum of two even numbers is even, you don’t walk through every pair of numbers. You reason about the structure, and the conclusion holds infinitely broadly.

The language MAGS uses for this is Dafny: a programming language with a built-in verifier, designed so that alongside your code you also write down precisely what has to be guaranteed.

What that looks like in practice

A minimal example — a function that writes a value to a computed index in an array:

method SafeWrite(a: array<int>, idx: int, value: int)
  requires 0 <= idx < a.Length            // assumption going in
  modifies a
  ensures a[idx] == value                 // promise coming out
  ensures forall i :: 0 <= i < a.Length && i != idx ==> a[i] == old(a[i])
{
  a[idx] := value;
}

Three things worth noticing:

requires is the condition the caller has to satisfy. If somewhere else in the code this function is called with an index Dafny can’t prove is in bounds, verification fails. Not with a warning you can wave away — the proof simply doesn’t go through.

ensures is the promise the function itself delivers. Dafny proves statically that every possible execution path satisfies it.

The second ensures is arguably the most interesting: it states that no other element changes. That’s a guarantee you’ll practically never nail down with testing, but which is straightforward to express formally.

Write <= where < belongs and you don’t get subtle behaviour that surfaces in production months later — you get an immediate error with a concrete counterexample.

What’s happening mathematically

Under the hood sits Hoare logic, named after Tony Hoare, who formalised it in 1969. The idea: a piece of code is a transformation between two logical statements, written as a triple:

$${P} ; C ; {Q}$$

Read it as: if $P$ holds before program $C$ runs, then $Q$ is guaranteed to hold afterwards. In our example, $P$ is the requires and $Q$ is the ensures.

The elegant part is that every language construct has a rule for combining such triples. For an assignment x := e, for instance, the rule works backwards: if you want $Q$ to hold afterwards, then before the assignment you need whatever you get by substituting e for x throughout $Q$. For sequential code: if ${P},C_1,{R}$ and ${R},C_2,{Q}$ both hold, then so does ${P},C_1;C_2,{Q}$. That’s how the guarantee gets assembled, as a chain of logical steps.

Dafny translates your entire program this way into one large logical formula — the verification condition — and hands it to an SMT solver (Z3, in this case). Such a solver is an automated proving machine that can establish whether a logical formula holds for all possible values, or else hand back a concrete counterexample. That counterexample is exactly what shows up as your error message.

Loops, and why induction is the crux

This is where it gets genuinely interesting. A loop can run an arbitrary number of times — you can’t possibly check each iteration separately. And yet the verifier has to be able to say something about it.

The answer is induction, the same principle you’d use to prove something holds for all natural numbers. You write a loop invariant: a statement that stays true on every pass through the loop.

method SumArray(a: array<int>) returns (sum: int)
{
  sum := 0;
  var i := 0;
  while i < a.Length
    invariant 0 <= i <= a.Length
    invariant sum == SumUpTo(a, i)     // stays true on every pass
  {
    sum := sum + a[i];
    i := i + 1;
  }
}

Dafny now only has to prove two things:

1. Base case — the invariant holds before the loop starts. With sum = 0 and i = 0, the sum of the first zero elements is indeed zero. Fine.
2. Inductive step — if the invariant holds at the start of an iteration, it holds again at the end. You add a[i] to the sum and increment i; the relationship survives.

Once those two are proven, the invariant automatically holds for any number of iterations. One, ten, or ten million — the mathematics doesn’t care. Combine the invariant with the exit condition (i == a.Length) and you’ve proven your final result.

That’s the whole trick: you replace an infinite number of checks with two finite proof steps. And that’s why verification is fundamentally different from testing very, very thoroughly.

It’s also where the friction lives. Coming up with the right invariant isn’t mechanical — it takes insight into what the loop is actually doing. Benchmarks like DafnyBench show this is where language models tend to stall: they write the code effortlessly, but the accompanying invariants remain a stumbling block, usually requiring several rounds of verifier feedback.

Back to MAGS

That’s where the paper’s approach comes together. MAGS is a multi-agent pipeline that automates this process:

1. Humans audit and “freeze” the APIs and safety requirements — these become the formal specification.
2. An agent translates the generated code into Dafny, annotations included.
3. When verification fails, the solver’s error message goes back to a repair agent, which adjusts the code or the invariant. That repeats until the proof lands — exactly the feedback loop that standalone models struggle with.
4. The verified version is compiled back into executable code.

The results: across 100 CUDA kernels, 100 terminal scripts and 20 robotic-arm tasks, MAGS achieves a 100% success rate in producing programs with non-trivial, verified safety guarantees against those frozen specifications.

The question that remains

One hundred percent sounds like an endpoint, but it isn’t — and the authors say so themselves. Failures still occur when the auto-formalized semantics don’t fully capture the intended behaviour.

That’s the heart of the matter, and it’s worth dwelling on. A proof is always a proof relative to a specification. Dafny guarantees, unforgivingly, that your code does what the requires and ensures say. Whether those say what you meant — nobody proves that.

So verification doesn’t so much solve the problem as relocate it: from “is this code correct?” to “is this specification correct?” That’s real progress, because a specification is shorter, more explicit and far more auditable than the implementation. But it’s also exactly why the MAGS pipeline has a step where a human pins down the requirements and freezes them.

As AI agents write more code than we can read, that’s probably where human judgement ends up moving. Not into reviewing every line, but into articulating what “safe” actually means — and writing it down sharply enough that a machine can check it.