Verified Code Generation: When the Model Has to Prove It

A coding model that passes every test you wrote is telling you something narrower than it sounds: it passes the tests you thought to write. Verified code generation closes that gap by demanding a different artifact, a machine-checked proof that the code satisfies a formal specification for all inputs, not just the handful in your test suite. The shift sounds like a niche academic concern until you notice what it does to the failure mode. With tests, an LLM's confident, plausible, subtly-wrong output slips through whenever your tests miss the case. With a proof obligation, the checker rejects it. The interesting consequence is not that verification makes models honest. It is that it relocates the hard problem, from "is this code correct" to "is this specification correct," and the second question is where the real difficulty (and the real LLM leverage) now lives.

This is the reality-gap argument applied to the most over-claimed capability in the field. The vibe-coding piece covers the productivity story; this is the correctness story, and the two diverge exactly where it matters. An agent that writes 2,000 lines an hour is worthless on a payment kernel if you cannot establish that the lines are right. Formal verification is how you establish it, and LLMs changed the economics of doing so.

Tests check examples; proofs check the claim

A unit test asserts that for a specific input, the output equals a specific value. A formal specification asserts a property over all inputs: this sort returns a permutation of its input that is ordered; this parser never reads out of bounds; this transfer preserves the total balance. A verifier (an automated theorem prover or proof checker) then establishes that the implementation satisfies the specification, or reports that it cannot. The guarantee is categorically stronger than a passing suite, because it is universally quantified rather than sampled.

This is the same structural idea that makes verifiable rewards work in training: a deterministic check you cannot talk your way around. The evaluation-crisis argument that a passing number is a hypothesis, not a result, has a clean answer in this one domain: a machine-checked proof is a result, because the checker is sound. The catch, which the rest of this article is about, is that the proof only certifies the code against the spec you wrote, and a wrong spec gets you verified-wrong code.

Two tools, two philosophies

The practical landscape splits along how much proof the human (or the model) has to supply.

Dafny is the auto-active end. You write the implementation plus annotations (preconditions, postconditions, loop invariants) and an SMT solver discharges the proof obligations automatically. When it works, you never write a proof by hand; you write the contract and the invariants and the solver does the rest. When it fails, it fails opaquely (the solver times out or cannot find the argument) and the human has to supply a stronger invariant. This is the sweet spot for LLM assistance, because inventing loop invariants is exactly the kind of pattern-shaped reasoning a model is good at and a human finds tedious. Recent work bears this out: DafnyPro (POPL 2026) reports 86% correct proofs on DafnyBench, the hardest benchmark of its kind, by having Claude Sonnet 3.5 generate and repair the annotations the solver needs, a 16-point jump over the same model without the framework.

Lean (specifically Lean 4 with its mathlib library) is the interactive-proof end, used for both mathematics and program correctness. Proofs are explicit objects the checker validates step by step, which gives maximal expressiveness and maximal effort. The LLM tooling here (LeanDojo for interfacing with proof states and retrieving relevant lemmas, Lean Copilot for in-editor suggestions) treats proof search as the task: given the current goal, propose the next tactic, check it, backtrack, repeat. This is where the most striking result lives. AlphaProof, an RL agent trained on millions of auto-formalized problems, reached silver-medal-level performance on International Mathematical Olympiad problems by searching for formal Lean proofs, learning the search the way a game-playing agent learns moves (the work is now published in Nature, 2025). The ceiling kept rising: by 2025, formal-proof systems in Lean reached gold-medal level at the IMO. Proof search is now a tractable reasoning target rather than a wall.

The two tools answer different questions. Dafny: can I verify this systems code without becoming a proof engineer? Lean: can I verify something whose correctness is genuinely deep? Both have become dramatically more usable because the part that scared people off (writing invariants, searching for proof steps) is the part LLMs now help with.

Autoformalization: the bridge and the bottleneck

There is a step before any of this that is easy to skip and decides everything: turning the informal intent ("sort this list," "this function never panics") into a formal specification the verifier understands. This is autoformalization, and it is simultaneously the bridge that makes LLM-assisted verification practical and the place the whole pipeline can silently break.

LLMs are now good enough at autoformalization to draft specs and translate problem statements into Lean or Dafny, which is what made benchmarks like CLEVER (curated, formally verified code generation) and the miniF2F-Dafny theorem-proving set possible to attempt at scale. But a generated specification is itself an unverified artifact. If the model formalizes "sorted" as "non-decreasing" but forgets the permutation requirement, the verifier will happily prove that a function returning an empty list is "correct," because the empty list is trivially non-decreasing. The proof is sound. The spec is wrong. Nothing in the verification pipeline catches it, because verification checks code against spec, never spec against intent.

This is the load-bearing honest tradeoff of the entire field: verification does not eliminate the trust problem, it concentrates it into the specification. The reason that is still a large win is that a spec is usually much smaller than the implementation, more stable, and reviewable by a human in a way that 2,000 lines of generated code is not. You move the thing you have to get right from a big artifact to a small one. But you do have to get the small one right, and "the LLM wrote the spec too" reintroduces exactly the risk you were trying to remove.

Where the cost is worth it

Formal verification has a real price (specification effort, annotation burden, solver runtime, and the expertise to read a failed proof) so it is not the default for a CRUD endpoint. The reality-gap question is where the cost clears, and the answer is the same as it has always been, now with LLMs lowering the price enough to widen the set.

It clears for code where a bug is expensive and the spec is expressible: cryptographic primitives, memory-safety properties in systems code, concurrency invariants, financial transaction logic, smart contracts, compiler and parser correctness. These share two features: the cost of a silent error is high, and the correctness property is something you can actually write down. Where the property is fuzzy ("the UI feels responsive," "the recommendation is good") there is nothing to formalize and verification has no purchase.

It also clears better in a loop than as a one-shot. The productive pattern is generate-then-verify-then-repair: an agent writes an implementation and a candidate spec, runs the verifier, reads the counterexample or failed obligation, and revises. The verifier is the reward signal, exactly the verifiable-reward structure that works elsewhere, which is why this is one of the few agentic settings where the feedback loop is tight and trustworthy rather than a demo waiting to break. The 2026 work pushes this structure harder: agentic verifiers (ATLAS, AxDafny, and agent-guided tree search over the solver's feedback) search over candidate annotations and proofs instead of one-shotting them, treating a failed obligation as a signal to branch rather than a dead end. The agent cannot bluff a sound checker, so the loop converges on code that actually satisfies the spec, with the standing caveat that "satisfies the spec" is only as good as the spec.

What to actually do with this

If you ship correctness-critical code and the property is expressible, verification is now reachable in a way it was not three years ago, and the move is to let the model carry the tedious part. Use Dafny-style auto-active verification when an SMT solver can plausibly discharge the obligations and the burden is invariants; use Lean when the correctness is deep enough to need explicit proof and lean on the proof-search tooling. In both cases, treat the LLM as the engine for invariants, tactics, and draft specs, and treat yourself as the reviewer of the one artifact that has to be right.

Concretely, run this decision procedure the next time an LLM hands you code you cannot afford to have subtly wrong:

1. Is the property expressible? Write the correctness claim as a sentence quantified over all inputs ("returns a permutation that is ordered," "never reads out of bounds," "conserves the total balance"). If you cannot, verification has no purchase here; fall back to tests and stop.
2. Is the stake high enough? Verification costs specification effort, annotation burden, and solver time. Spend it only where a silent error is expensive: crypto, memory safety, concurrency, financial logic, compilers, smart contracts.
3. Pick the tool by the depth of the proof. Obligations an SMT solver can plausibly discharge (the burden is invariants) go to Dafny; correctness deep enough to need explicit proof objects goes to Lean.
4. Write the spec yourself, or review the model's spec line by line. This is the artifact the verifier never checks against intent. Draft it with the LLM if you like, but treat the draft as unverified until you have read every clause and asked what a vacuous or trivial implementation would satisfy.
5. Run the generate-verify-repair loop. Let the model produce the implementation plus annotations or tactics, run the verifier, feed the counterexample or failed obligation back, and iterate. The checker is the reward signal; the agent cannot bluff it.
6. Adversarially test the spec, not just the code. Ask whether an obviously wrong implementation (the empty list, the identity function, the no-op) passes your spec. If it does, the spec is incomplete, and the green checkmark is lying to you.

And put your scrutiny where the risk concentrated. Review the specification harder than you review the code, because the verifier already reviewed the code against the spec and reviewed nothing about whether the spec captures intent. A verified system with an unexamined spec is not a verified system; it is a very confident one. The discipline that distinguishes real assurance from theater is the same as everywhere else in this field: name what was actually checked, against what reference, and treat the unchecked link (here, spec versus intent) as the place the next failure comes from.

Key Takeaways

1. Passing tests checks examples; a proof checks the claim. A formal specification asserts a property over all inputs, and a verifier establishes the code satisfies it universally, which is categorically stronger than any test suite.
2. Verification relocates the hard problem to the spec. It does not make the model honest; it moves the thing you must get right from a large implementation to a smaller specification, then certifies the code against that spec.
3. A wrong spec yields verified-wrong code. The checker is sound, so it will prove a function correct against a spec that omits a requirement. Verification never checks the spec against your actual intent.
4. Dafny and Lean answer different questions. Dafny (auto-active, SMT-discharged) suits systems code where the burden is invariants; Lean (interactive, explicit proofs) suits deep correctness. LLMs now carry the tedious part of both.
5. The results are real. DafnyPro reports 86% on DafnyBench by generating and repairing annotations, and AlphaProof reached IMO silver-medal level by searching for formal Lean proofs, evidence that proof search is now tractable.
6. Autoformalization is the bridge and the bottleneck. LLMs can draft specs and formalize intent, which makes the pipeline practical, but a generated spec is itself unverified and is exactly where silent failures enter.
7. The cost clears for high-stakes, expressible properties. Crypto, memory safety, concurrency, financial logic, compilers. Where the property is fuzzy, there is nothing to formalize and verification has no purchase.
8. Verify in a loop, and review the spec hardest. Generate-then-verify-then-repair is a tight, trustworthy feedback loop because a sound checker cannot be bluffed. Put your scrutiny on the specification, the one link the verifier never checks.

The Acing AI newsletter covers AI-for-code by what it can actually guarantee, not what the demo implies. Subscribe for the version that names what was checked.