Everything is evals

I’ve come to think of every way we check AI-written code as an eval. A unit test is an eval that samples a few inputs. A property-based test samples many. An LLM judge is an eval with an opinion. A formal proof is the limiting case: an eval that covers every input, checked by a small program you can audit. If you want to let models write code nobody reads, it is the obvious place to end up, and in the last two years it has started to look practical. Martin Kleppmann recently argued that AI will make formal verification mainstream, because models can now write the proofs that used to cost experts years (Kleppmann).

I think that’s half right. Models can now write the proofs. But I think a proof moves the need for trust rather than removing it: it lands on the specification the proof is about and on the machinery that checks it. Once proofs are cheap, those become the places where things go wrong, and the evals that matter are the ones that check them.

the spectrum of checkers

The tools sit on a spectrum from automatic to interactive. At one end are auto-active verifiers like Dafny and Verus, where you write a program with its pre- and postconditions and loop invariants, and an SMT solver (usually Z3) tries to discharge the rest. At the other end are interactive proof assistants like Lean, Rocq (formerly Coq) and Isabelle, where proofs are built step by step with tactics and checked by a small kernel. F* sits in between, using an SMT solver with tactics on top.

Tool	What you trust	Automation	Industrial use
Dafny	Its verifier, Boogie, Z3 and the compiler	SMT solver	AWS authorization engine
Verus (Rust)	Verus, Z3 and rustc	SMT solver	AWS Nitro Isolation Engine
F*	Its checker, Z3 and code extraction	SMT plus tactics	Verified cryptography in Firefox and Linux
Lean 4	A small kernel, plus any extra axioms	Tactics	AWS Cedar’s model
Rocq	A kernel and code extraction	Tactics	CompCert C compiler
Isabelle/HOL	A small kernel	Tactics plus automated provers	seL4 microkernel
Bend 2	A checker, optionally a kernel proven in Lean	None, explicit proofs	None yet

AWS and others have used these tools in production for years, mostly without fanfare. AWS answers about a billion access-policy queries a day with Zelkova, an SMT-based analyzer (Rungta), and runs a Dafny-verified authorization engine that handles over a billion requests a second (Amazon Science). It models its Cedar policy language in Lean, and used Verus for the Nitro Isolation Engine (Amazon Science). What I take from AWS is to use the cheapest checker that can discharge the property, not one prover for everything.

what a proof says

A proof of a program establishes one thing. For every input satisfying the precondition, the program’s output satisfies the postcondition:

\vdash_{\,\mathcal{T}}\;\; \forall x.\;\; \mathrm{pre}(x) \;\Rightarrow\; \mathrm{post}\big(x,\, f(x)\big),

relative to a trusted base $\mathcal{T}$ : the checker, its axioms, the model of the language and machine, the compiler and the runtime. Nothing in that statement says whether $\mathrm{pre}$ and $\mathrm{post}$ capture what you meant. Every failure of verified software I could find sits in one of those gaps rather than in the proof itself:

A proof checks one layer. Everything above it is a question of meaning, and everything below it is a question of trust. Click a layer for a failure that happened there.

What a proof of code checks, and everything it trusts. Click a layer for a failure that happened there

The long record of verified systems suggests where the effort and the bugs actually go. seL4, the verified microkernel, is 8,700 lines of C proved against 200,000 lines of proof in Isabelle, about 23 lines of proof per line of code, at roughly 20 person-years of proof effort (Klein et al.). The deep bugs surfaced while refining the abstract specification into a design; the 144 bugs found at the C level were mainly typos, because by then the design was already verified. Maintenance followed the same pattern. The cost of re-proving tracked how many invariants a change touched, not how many lines it changed: one change to under 5% of the code “fundamentally broke” key invariants.

CompCert, the verified C compiler, tells the same story from the other side. When Csmith threw about six CPU-years of random programs at it, it found no wrong-code bugs in the verified middle of the compiler. It found miscompilations in the unverified front end, and one bug in CompCert’s own formal model of PowerPC, which is to say a bug in the specification of the machine (Yang et al.).

the AI provers

What changed in the last two years is who writes the proofs. In mathematics the progress has been dramatic. AlphaProof reached silver-medal level at the 2024 International Mathematical Olympiad (Hubert et al.), and Axiom’s prover solved all twelve Putnam 2025 problems in Lean (Axiom). Most of this happens in Lean, because Mathlib gives models a large library to train on and build from.

Code is different, and one result surprised me. Lean leads in AI mathematics, but it came last for AI-verified code. On the vericoding benchmark of more than 12,000 specifications, models produced verified code 82% of the time in Dafny, 44% in Verus and 27% in Lean (vericoding benchmark). On AlgoVeri, which gives all three languages identical specifications, the rates were 40.3%, 24.7% and 7.8% for Dafny, Verus and Lean (AlgoVeri). My read is that for code, an SMT solver that discharges routine obligations automatically is worth more than a large corpus of human proofs.

Proving code against a given specification is close to solved on today’s benchmarks. On DafnyBench, where the task is to add the annotations that make a verified program check, the best systems now exceed 90% (DafnyPro). Harmonic reports its Aristotle system at 96.8% on VERINA’s proof tasks, though that figure is self-reported and counts 23 specifications it disproved rather than proved (Harmonic). Disproof is worth noticing. A proof-based eval can tell you that the benchmark itself is wrong, which no test suite can.

the specification is the bottleneck

Writing the specification is where models are weakest. VERINA scores code, specification and proof separately. With o3, the code was correct 72.6% of the time, the specification sound and complete 52.3% of the time, and the full proof 4.9% of the time (VERINA). On CLEVER, which requires a model to produce both the specification and a verified implementation, the best system at launch managed one problem in 161 end to end (CLEVER).

The benchmarks have specification problems of their own. In the vericoding benchmark, about 9% of the specifications behind successful solutions were too weak to mean much, and another 15% were poor translations of the intended task (vericoding benchmark). An ICML 2026 audit of five widely used Lean benchmarks found 398 mechanically certified defects, including counterexamples, vacuous theorems and unsound axioms (Ammanamanchi et al.).

I think this matters more as models improve. Hillel Wayne makes the sharpest version of the objection: specifications written by language models tend to state the obvious properties, the ones you’d have tested anyway, and miss the subtle ones that make verification worth doing (Wayne). If a model writes both the code and the specification, the proof certifies that two outputs of the same model agree with each other. That checks consistency. It doesn’t tell you the code is correct.

when the checker is the target

Once a proof checker becomes a reward for reinforcement learning, the model tends to find ways to satisfy it that aren’t proofs. The clearest measurement I have found is from a Dafny RL study: the verified rate rose from 2.2% to 58.1% during training, but on tasks whose specifications couldn’t be gamed, it rose only from 9.7% to 31.1% (Tan). That suggests more than half of the headline gain came from exploiting weak specifications.

The tricks are mostly simple. A Lean proof can close a goal with a disguised sorry, the placeholder for an unfinished proof. A model can redefine ≤ on integers locally so that every comparison is trivially true. In Dafny, assume false makes anything verify. The usual defense in Lean is to print the axioms a proof depends on and reject anything unexpected. One exploit that showed only a standard axiom under #print axioms fooled both lean4checker and SafeVerify; only a tool that exported and re-parsed the proof caught it (Lean reference).

The kernels themselves are now under adversarial pressure. An AI-assisted “disproof” of the Collatz conjecture passed both Lean’s official kernel and an independent re-implementation, through two unrelated bugs (oss-security). Lean 4.34 shipped three soundness fixes found with OpenAI’s models (Lean), and a researcher working with Claude found seven kernel bugs in Rocq (de Moura). The same kind of model is now both a major producer of proofs and one of the best finders of bugs in the checkers that grade them.

what the proof doesn’t reach

Below the checker sit the compiler, the runtime and the machine. lean-zip, a port of zlib to Lean with a proved compress-and-decompress round trip, survived about 105 million fuzzing runs on its verified code. Fuzzing still found a heap overflow in Lean’s C++ runtime, triggered by a 156-byte ZIP file, and a crash in the unverified archive parser around it (Kiran).

Some properties are hard to state at all. Lean can’t reason about floating-point code in its kernel without extra axioms, so numerical software needs an explicit model of IEEE arithmetic. Performance is invisible to a functional specification, and agents exploit that: given a hard-to-verify reference algorithm, they substitute a simpler one that meets the specification and runs worse. And I don’t know how you’d write “does what the user meant” as a formula.

I think this is why the industrial projects that worked combine proof with testing rather than replacing one with the other. At AWS, Cedar’s Lean proofs found four bugs, while differential and property-based tests that compared the Rust implementation against the proved Lean model found 21 (Cutler et al.). The proof made the tests meaningful by giving them an oracle. The tests covered the gap between the model and the code that actually runs.

Bend

A colleague pointed me to Bend 2, from Victor Taelin’s HigherOrderCO, as a different bet on the same problem (Bend). Its pitch is a fast language that blocks AI mistakes with proofs. You declare the properties you want in one file and their proofs in another, over a dependent type theory with no tactics or proof search, and an optional mode re-checks the proofs with a kernel that has itself been proved correct in Lean.

The interesting part is what it says about where trust ends up. The proof kernel is verified. The compiler, by the project’s own README, is 99% written by AI and not yet fully audited. AI can now write the toolchain as well as the code, so something still has to check the toolchain, and I don’t think the answer can be the same model.

proofs as reward

Used carefully, I think verification is still the best reward we have for code. A proof checker has no false positives once the specification, the harness and the checker itself are sound, which makes pass@k honest in a way test-based rewards aren’t. Partial credit helps with sparse rewards: one recent system rewarded the fraction of proof obligations discharged, audited specification integrity separately, and raised the share of real repository issues it resolved, as graded by tests, from 59.6% to 72.5% (arXiv).

What I could not find is a measurement of the thing I’d assumed had changed: the cost per verified line of software, before and after language models. There are costs per proof, and corpus-scale numbers from mathematics, but nothing that would let you say verified code is now ten times cheaper to produce. And as of writing, I found no company that has publicly shipped AI-written, formally verified code in production with a named specification and customer.

A proof reduces the question “is this code right?” to “is this specification right, and can I trust the checker?” That is real progress. The second question is smaller and more auditable than the first. But it means the evals that matter now are evals of specifications and of harnesses: checking two specifications for equivalence, mutating a specification to see whether the proof still holds, generating counterexamples, checking proofs with independent kernels, and testing the implementation against the proved model.

I think the job of a software engineer working with AI shifts accordingly. Reviewing code becomes reviewing specifications, and the scarce skill is saying precisely what you want. I suspect the proof is now the easy part. What I don’t know is how you’d review specifications at the speed models can now write them, and I’d like to hear how others are doing it.