What Software Can We Verify Today?, Part 1

In April 2014 the internet learned that for two years OpenSSL had been answering a simple question dishonestly. A TLS heartbeat says "here are three bytes, please echo them back, and by the way they are 64 kilobytes long." OpenSSL believed the length, copied 64 kilobytes out of its own heap, and sent back whatever happened to be there: session cookies, passwords, private keys. The fix for Heartbleed was one bounds check. The code had been read, reviewed, fuzzed, and deployed on a large fraction of the web's servers, and nobody had written down, in a form a machine could check, that the advertised length must fit inside the packet.

Twelve years later, Claude, asked by Anthropic's Frontier Red Team and the startup Theorem to prove that open-source decompression and image libraries never crash, found a counter underflow that corrupts memory only on inputs of around 20 megabytes, exactly the kind of bug a fuzzer is unlikely ever to reach. The proof attempt failed, and the failure was the finding. That is the promise of AI-driven verification in one sentence, and this post is about how far it reaches.

Machines now synthesize thousands of lines of C, Rust, or Python in minutes, while human review is still limited by reading speed and fatigue. That gap is a verification deficit, and it is the context for everything below.

I trust AI-generated code the way I trust code an exhausted junior engineer wrote at 2 a.m.: not at all, until a deterministic system has checked it.

Figure 1 is the argument in one frame: routes from source code into Lean 4, and the bottlenecks that remain.

01 Cheap Proofs, Expensive Software

Formal verification has been the candidate answer for half a century. A test suite can only show the presence of the bugs someone thought to test for; a proof covers every input and every path against a precise specification. The trouble was always cost. The functional-correctness proof of the seL4 microkernel cost about 20 person-years in total, including some 9 person-years of reusable tooling, for roughly 8,700 lines of C. That works out to half a specialist person-day per line of implementation.

Writing the kernel took about 2.2 person-years; proving it took roughly nine times as long, and the hand-written proof ended up more than twenty times the size of the code it covers. What that bought was functional correctness: a machine-checked proof that the C code always follows its abstract specification of kernel behavior. The usual safety properties fall out of it as corollaries. The kernel never crashes, never dereferences a null or misaligned pointer, never violates an assertion on any code path, and every system call terminates and returns to user level. The guarantee is conditional, though. The proof assumes the compiler, the assembly code, the boot code, cache management, and the hardware are correct, and proves everything else. Figure 2 makes the cost split concrete.

The current thesis, argued by Martin Kleppmann and by Lean's creator Leonardo de Moura in an essay on who verifies AI-written software, and by DARPA, ARIA's Safeguarded AI programme, and a run of startups, rests on an asymmetry. When a model hallucinates in Python, the hallucination ships unless a test or reviewer catches it. When it hallucinates in a Lean proof script, the small trusted kernel rejects the term and the agent tries again. Hallucinations become retries rather than vulnerabilities.

That asymmetry explains the medal-level Olympiad results from DeepMind's AlphaProof and Harmonic's Aristotle. It does much less for software, because full automation asks for more than a proof. Depending on the benchmark, a model with no human in the loop must produce some or all of three artifacts that have to agree: (1) an implementation, (2) a formal specification of what it should do, and (3) a proof that the implementation satisfies the specification.

Each artifact can sink the others. If the implementation has a subtle bug, the theorem is false and no number of retries will prove it; the kernel says no, but not whether to fix the code, the specification, or the proof. Even correct code needs loop invariants, termination measures, and lemmas about arrays and bounded integers before a proof goes through. Dafny and Verus hand most of those obligations to an SMT solver, while in Lean the model writes far more of the proof itself, which I suspect is part of why Lean trails both. And the kernel checks the proof against the theorem as stated, not against what anyone meant, so a vacuous specification passes as easily as a correct one. The retry loop converges only when there is a provable, meaningful target to converge on.

The benchmark numbers bear this out. On the multi-language vericoding benchmark, the best of nine off-the-shelf models, given five attempts each with verifier feedback, solved 68% of Dafny tasks, 31% of Verus tasks, and 18% of Lean tasks; pooled across all nine, the figures rise to 82%, 44%, and 27%. On CLEVER, an end-to-end verified code generation benchmark in Lean, the best baseline solved one problem in 161, although a later audit disputes half of CLEVER's own reference specifications.

On VERINA the best model wrote correct code 73% of the time, a sound and complete specification 52% of the time, and a correct proof 5% of the time. And when a task needs reasoning across function boundaries, the DafnyComp benchmark shows verification success falling to about 3.7%, against 58–68% on single-function Dafny benchmarks.

So the question this post asks is narrower than "can AI do formal methods?" It is: which software can we actually get into Lean, and prove something non-trivial about, today?

02 Why Lean, and Why Now

To see why Lean 4 is both the prize and the bottleneck, it helps to place it among the tools that came before it. Verification tools have always traded off three things against each other: how much they can express, how much they automate, and how much human effort they demand.

The Verification Triangle

Each family of tools sits at a different point on that trade-off, and Figure 3 places them on it.

Push-button static analyzers and model checkers sit at the automated corner. Abstract interpreters such as Astrée and Frama-C's Eva plugin, bounded model checkers such as CBMC and ESBMC, and software model checkers such as CPAchecker run directly on C or Java and prove bounded safety properties: no buffer overflow, no null dereference, no division by zero. They struggle with deep loops and complex heaps, and they cannot state a rich property such as "this scalar multiplication implements the group law over the field of size 2²⁵⁵ − 19."

Auto-active verifiers hold the middle. In Dafny, Verus, Why3, Viper, or Frama-C/WP, developers annotate code with requires, ensures, invariant, and decreases clauses; the tool turns the annotated program into verification conditions and hands them to an SMT solver such as Z3 or cvc5. When the solver succeeds it feels like magic. When it times out on nonlinear arithmetic or alternating quantifiers, the developer is left with brittle solver heuristics and no interactive way to steer the proof.

Foundational interactive provers, Lean 4, Rocq, and Isabelle/HOL, sit at the expressive apex. There is no ceiling on what Lean can state, from Galois theory to the semantics of a hypervisor, and every proof, however it was found, is reduced to a term checked by a small kernel. You do not have to trust a half-million-line SMT solver or a verification-condition generator. The price, historically, was crushing manual effort: engineers wrote tactic scripts (intro, induction, simp, omega) one step at a time.

Why Lean Became the Center of Gravity

Given that Dafny produces far higher success rates than Lean, why are Harmonic, &Truth, Axiomatic AI, AWS, and much of academia converging on Lean? Five properties explain it.

• Mathlib. Verifying cryptography, numerics, control filters, or consensus needs real mathematics. Mathlib has nearly 300,000 formalized theorems. That depth is part of why a partial result on the Riemann hypothesis (Claude's 2026 67.2% lower bound for the fraction of zeta zeros on the critical line) could be formalized at all. In Dafny or Verus the same background theory has to be axiomatized, which risks unsoundness, or re-proved by hand.
• One language for everything. Lean 4 is a dependently typed functional language that compiles to C, and its macro and metaprogramming framework is written in Lean itself. That lets researchers embed imperative verifiers (Velvet, Veil), SMT bridges (lean-smt, lean-auto), proof search (Aesop), and property-based testing (Plausible) inside Lean without enlarging the trusted kernel.
• Dense feedback. Z3 says "proved" or "timeout." Lean's language server exposes the exact goal state after every tactic, every hypothesis and every remaining subgoal. That turns proving into a sequential decision problem that tree search and reinforcement learning can work on.
• Built-in imperative reasoning. Lean now ships its own monadic verification-condition generator, mvcgen, for ordinary do-notation code. Given a program with mutable variables, loops, and early returns, plus a pre- and postcondition, it breaks the goal into the kind of proof obligations Dafny would hand to Z3, leaving the loop invariants and the arithmetic to be supplied. That targets the gap I suspect explains part of Lean's lag behind Dafny and Verus: the model no longer has to hand-write the plumbing of Hoare logic. Because mvcgen is a tactic, everything it produces is still checked by the kernel, so the trusted base does not grow. It is new enough that models had barely seen it in 2025: the vericoding Hoare-triple tasks written for it were solved 8% of the time. I read that number as unfamiliarity rather than difficulty, and unfamiliarity is a gap that training data closes.
• No expressivity cliff. In Lean, automation (grind, omega, aesop, lean-smt) can discharge the routine obligations and leave the hard ones, such as inductive invariants or nonlinear modular arithmetic, as ordinary goals that an AI prover or a human can close. An SMT-only pipeline stops.

The trade-off is visible in the vericoding numbers. The benchmark hands a model a formal specification, so what "correct" means is already settled, and asks for an implementation plus a proof that it meets the specification, in Dafny, Verus, or Lean. With the specification written for it, the model is measured on the cost of the proof language alone.

Each of nine off-the-shelf models had five attempts per task with verifier feedback (ten on the BigNum subset), on 2,161 to 2,361 tasks per language. The task sets differ in size and content, so cross-language comparisons are approximate, but the ordering never changes: Lean buys expressivity and a small trusted base, and it pays for them in success rate, for every one of the nine models tested. The numbers also move fast; the same paper reports that LLM success on pure Dafny verification rose from 68% to 96% in a year. Figure 4 shows the gap by target language.

Olympiad Problems Are Not Software

Why do AI provers ace Olympiad algebra in Lean and fail on most software benchmarks? Because the two kinds of problem barely resemble each other.

An IMO problem fits in five lines using definitions that already exist in Mathlib. A 500-line C or Rust module depends on fixed-width integers, pointer aliasing, heap layout, I/O, error codes, and dozens of project-specific types and helpers. Software is overwhelmingly imperative and stateful, while Lean's logic is pure and total: every function must terminate and mutation does not exist at the logical level.

And software proofs are procedural. In their study of neural proof generation on seL4, He et al. found that the proofs lean on domain-specific weakest-precondition tactics whose meaning lives in the prover's internal state rather than the script's text. To show what that does to a model, they asked Gemini 3 Pro and GPT-5.1 to re-prove one seL4 theorem whose human-written proof already exists, with web search disabled so neither could look the original up. Both recognized they were inside an seL4 proof, and both failed. They could not drive wp, the tactic that computes the weakest precondition of a kernel operation and is the workhorse of these proofs, and they cited lemmas that do not exist in the library, such as a plausible-sounding hoare_seq_ext. Feeding the prover's error messages back for several rounds of repair did not rescue either proof.

Bridging that gap raises a problem pure mathematics never has: how does normal software get into Lean in the first place?

03 Five Ways Into Lean

You cannot feed a .c or .rs file to the Lean kernel. Every AI-assisted verification pipeline therefore commits to a translation trajectory, an architectural path that transforms or embeds the source into Lean. Across research and the commercial platforms (Harmonic, &Truth, Theorem, Runtime Verification, Galois) five trajectories have emerged, and each makes a different bet about where the AI sits, what lands in the trusted computing base, and what the proof obligations look like. Figure 5 lays out the five routes.

A: Direct LLM Rewrite

The most direct route uses the model as an unverified transpiler. It is also what standard benchmarks such as VeriBench and CLEVER measure. Given a specification or an existing function, the model writes a pure Lean implementation, a formal specification, and a proof. Start with an ordinary C binary search:

int64_t binary_search(const uint64_t *arr, size_t n, uint64_t target) {
    size_t low = 0;
    size_t high = n;
    while (low < high) {
        size_t mid = low + (high - low) / 2;
        if (arr[mid] == target) {
            return (int64_t)mid;
        } else if (arr[mid] < target) {
            low = mid + 1;
        } else {
            high = mid;
        }
    }
    return -1;
}

The model rewrites the loop as a terminating recursive function over Array UInt64, threading bounds proofs through the indices:

-- Trajectory A: direct functional rewrite in Lean 4
def binarySearchAux (arr : Array UInt64) (target : UInt64) (low high : Nat)
    (h_bound : high ≤ arr.size) : Option (Fin arr.size) :=
  if h : low < high then
    let mid := low + (high - low) / 2
    have h_mid : mid < arr.size := by omega
    let val := arr[mid]'h_mid
    if val == target then
      some ⟨mid, h_mid⟩
    else if val < target then
      binarySearchAux arr target (mid + 1) high h_bound
    else
      have h_mid_le : mid ≤ arr.size := by omega
      binarySearchAux arr target low mid h_mid_le
  else
    none
termination_by high - low
decreasing_by
  all_goals simp_wf; omega

When this works the result is clean and amenable to induction. That is how AWS built Cedar, its authorization policy language: the reference model, first in Dafny and later in Lean, was proved against its security properties, and the production Rust implementation was checked against it by differential testing. But as a way to verify existing software it has two problems.

First, there is an unverified semantic gap. You have proved the Lean rewrite, not the C that runs in production. A bug such as low + high overflowing size_t can be silently "fixed" when the model maps size_t to Lean's unbounded Nat.

Second, single-mode synthesis converges poorly. In the LeetProof evaluation of 50 imperative-style problems on a $5-per-problem GPT-5.2 budget, direct Lean synthesis fully proved only 17. When the model picks a slightly unidiomatic recursion, the proof obligations tangle with dependent casts and termination proofs that the prover cannot discharge.

VeriBench puts the problem in one number: its strongest coding agents get their Lean to compile every time and state the theorems the task calls for about one time in ten. Route A done well looks different. In de Moura's essay, Lean FRO engineers had a general-purpose agent write a zlib implementation in Lean and prove that decompression inverts compression at every level: a new implementation with a short specification, making no claim about the original C.

B: Compiler Lifting for Rust

What if the clean functional Lean of route A could come from a compiler pass instead of a guess? That is the idea behind Aeneas, from Son Ho and Jonathan Protzenko, together with the Charon frontend (Cryspen's hax now targets Lean through the same Charon and Aeneas pipeline; its best-known production result, the ML-KEM proofs in libcrux, is in F* rather than Lean).

Verifying imperative code in a proof assistant traditionally means reasoning about a mutable heap with separation logic, which is powerful and heavy. Aeneas observes that safe Rust has already done the alias analysis: a &mut T is guaranteed exclusive for its lifetime. So a function that mutates through &mut T can be translated into a pure function that takes the old value and returns the new one, with no heap model at all. Charon hooks into rustc and lowers MIR into a typed intermediate form (LLBC); Aeneas then turns each function into a pure Lean function in a Result monad that models success, panic, and divergence. Take this ordinary Rust:

pub enum Op { Add, Sub }
pub enum CalcError { Overflow, Underflow }

pub fn apply_op(acc: &mut u64, op: Op, arg: u64) -> Result<u64, CalcError> {
    match op {
        Op::Add => {
            if *acc > u64::MAX - arg {
                return Err(CalcError::Overflow);
            }
            *acc = *acc + arg;
            Ok(*acc)
        }
        Op::Sub => {
            if *acc < arg {
                return Err(CalcError::Underflow);
            }
            *acc = *acc - arg;
            Ok(*acc)
        }
    }
}

The extracted Lean looks like this. The mutable reference becomes an input plus an updated output in a tuple, and the machine arithmetic is preserved: acc + arg fails inside the monad unless you prove it fits in 64 bits.

import Aeneas
open Aeneas.Std

inductive Op where
| Add : Op
| Sub : Op

inductive CalcError where
| Overflow : CalcError
| Underflow : CalcError

def apply_op (acc : U64) (op : Op) (arg : U64) :
    Result (Core.Result.Result U64 CalcError × U64) :=
  match op with
  | Op.Add => do
    let max_sub ← core.u64.max - arg
    if acc > max_sub then
      ok (Core.Result.Result.Err CalcError.Overflow, acc)
    else do
      let acc1 ← acc + arg
      ok (Core.Result.Result.Ok acc1, acc1)
  | Op.Sub =>
    if acc < arg then
      ok (Core.Result.Result.Err CalcError.Underflow, acc)
    else do
      let acc1 ← acc - arg
      ok (Core.Result.Result.Ok acc1, acc1)

No model touched the translation. The AI enters only to write the specification and the proof, using Aeneas's progress and scalar_tac tactics. This is the cleanest way to verify safe Rust in Lean today. Microsoft is using it on its Rust rewrite of SymCrypt, the Beneficial AI Foundation has an ongoing (still sorry-bearing) verification of curve25519-dalek, and Runtime Verification has written up its use on polynomial arithmetic.

The limits are clear too. Unsafe code, raw pointers, SIMD intrinsics, and interior mutability (RefCell, Mutex) fall outside the borrow-calculus fragment; RefinedRust handles unsafe Rust with separation logic in Rocq, at the cost of exactly the heap model Aeneas avoids. Generic code with heavy trait bounds often needs monomorphizing first, and extracted loops still need termination measures. Calls into external crates and the OS are opaque unless axiomatized. And in practice Aeneas, Mathlib, and Batteries pin different Lean toolchains, so version drift and name collisions can stall a pipeline before a single tactic runs.

C: An Imperative Language Inside Lean

If route A is too far from imperative code and route B only covers safe Rust, the third option is to bring the imperative language into Lean. Velvet (for algorithms) and Veil (for transition systems and distributed protocols), from Ilya Sergey's VERSE lab at NUS, embed a Dafny-like language as a shallow monadic DSL. You write method … requires … ensures … do inside a .lean file, and underneath it is a stack of ordinary Lean monads with ghost state.

The foundations are published: Velvet itself appeared at CAV 2026, and the Loom framework underneath it derives the weakest-precondition generator for each monad stack automatically, with a soundness proof, so the VC generator is not part of the trusted base.

Because the result is ordinary Lean, a single program can be checked several ways: executed with #eval or #guard, tested against its own contract through Plausible, pushed through a weakest-precondition generator with SMT, and, for whatever automation leaves behind, handed to an AI prover as a named Lean goal with Mathlib available. Here is a loop with its invariants:

import Velvet

-- Trajectory C: imperative program embedded in Lean 4 via Velvet
method sumUpTo (n : Nat) returns (acc : Nat)
  ensures 2 * acc = n * (n + 1)
do
  let mut i : Nat := 0
  acc := 0
  while i < n
    invariant i ≤ n
    invariant 2 * acc = i * (i + 1)
    decreases n - i
  do
    i := i + 1
    acc := acc + i
  return acc

-- 1. cheap dynamic check
#guard (sumUpTo 10).run == 55

-- 2. VC generation + automation; residual goals stay ordinary Lean goals
prove_correct sumUpTo by
  velvet_vcgen [sumUpTo]
  all_goals omega

Route C and route A diverge sharply in practice. On the same 50 problems, the same specifications, and the same $5 budget, LeetProof on Velvet fully proved 28 against single-mode Lean's 17. The more striking result is what happened next: handed the partially proven attempts, Aristotle closed all 18 Velvet partials, for 46 of 50 certified, while seven of the single-mode partials resisted even Aristotle. Figure 6 shows where the 50 problems landed.

The reason is ordering. In the Velvet pipeline, property-based testing exercised both the implementation and the candidate invariants on thousands of random inputs before any expensive proof search began. By the time an obligation reached the prover, it was almost certainly true.

D: Lifting Unmodified Source

In avionics, automotive, hardware RTL, and legacy systems code, nobody is going to rewrite the product into Rust or a Lean DSL. The artifact stays in C, Verilog, or Java. Route D keeps the source unmodified and uses a deterministic frontend to lift its AST into an explicit state machine or deep embedding inside the prover.

Three incarnations show the range. Harmonic has extended Aristotle to C and Verilog. For hardware it has described the mechanism: SystemVerilog and its assertions are compiled into Lean through a hand-built model of digital circuits, explicitly not by LLM transliteration, and it used this to prove the multiply and divide units of the Ibex RISC-V core. For C it claims functional correctness and the absence of classes of undefined behavior, with LibTomMath as the case study, but has not described how C is lifted.

The seL4 project's AutoCorres shows that a lifter need not be trusted at all: it emits a proof alongside each C-to-Isabelle abstraction, leaving only the C parser and the compiler in the base. Forge, from Wei et al., is documented: it takes safety-critical Java written in an extraction-friendly profile, lifts it through Spoon and EMF into a RoboChart state machine, and emits Dafny, CSP for FDR4, and Isabelle artifacts, followed by a vacuity audit. Failures become structured repair prompts for the Java.

What does a lifted program look like? Take a parser in the spirit of Heartbleed (CVE-2014-0160), which reads a 16-bit length from a request and copies that many bytes out:

int process_heartbeat(const uint8_t *req, size_t req_len,
                      uint8_t *resp, size_t max_resp_len) {
    if (req_len < 3) return -1;  // 1 byte type + 2 bytes payload_len
    uint16_t payload_len = ((uint16_t)req[1] << 8) | (uint16_t)req[2];

    // the Heartbleed patch: the advertised length must fit in the request
    if ((size_t)payload_len + 3 > req_len) return -1;
    if ((size_t)payload_len > max_resp_len) return -1;

    for (size_t i = 0; i < payload_len; i++) {
        resp[i] = req[3 + i];
    }
    return (int)payload_len;
}

A route-D lifter cannot ignore integer widths or out-of-bounds reads. It produces an explicit execution state and models every dereference as a checked step that enters an undefined-behavior state when it goes out of bounds:

structure CBuffer where
  data       : Array UInt8
  size_bound : data.size ≤ USize.size.toNat

inductive CExecResult (α : Type) where
  | ok : α → CBuffer → CExecResult α
  | ub : String → CExecResult α   -- undefined behavior is a value, not a hope

def readUInt8 (buf : CBuffer) (idx : USize) : Except String UInt8 :=
  if h : idx.toNat < buf.data.size then
    .ok (buf.data[idx.toNat]'h)
  else
    .error "heap buffer over-read"

def process_heartbeat_lifted (req : CBuffer) (req_len : USize)
    (resp : CBuffer) (max_resp_len : USize) : CExecResult Int32 :=
  if req_len < 3 then .ok (-1) resp
  else
    match readUInt8 req 1, readUInt8 req 2 with
    | .ok b1, .ok b2 =>
      let payload_len : UInt16 := (b1.toUInt16 <<< 8) ||| b2.toUInt16
      if payload_len.toUSize + 3 > req_len || payload_len.toUSize > max_resp_len then
        .ok (-1) resp
      else
        -- lifted copy loop over a bounded state transition …
        sorry
    | _, _ => .ub "out-of-bounds header read"

Memory safety is now a theorem: for all buffers whose declared lengths match their allocations, the lifted function never returns ub. Delete the bounds check and the theorem becomes false, and a counterexample search can hand back the exact three-byte packet ([0x01, 0x00, 0x01] with req_len = 3) that triggers a read at index 3.

E: Lifting the Binary

Every route so far trusts a compiler. What if Clang, GCC, or rustc miscompiles, optimizes away a check because of undefined behavior, or links in hand-written assembly? Route E takes the compiler out of the trusted base by lifting the compiled binary into a formal model of the instruction set and the OS interface.

AWS's LNSym is a symbolic simulator for Armv8 machine code written in Lean, exercised on cryptographic routines from AWS-LC. Theorem (theorem.dev) applies the same idea at far larger scale, though in Rocq rather than Lean: with Anthropic, it lifted RISC-V builds of 123 open-source libraries into a model of the ISA and Linux process semantics and had Claude prove them crash-free, a result covered in the case study in Part 3. Google DeepMind's AlphaProof Code, announced on November 10, 2026, stays in Lean and aims past crash-freedom: it compiles Signal's unmodified libsignal with stock rustc, loads the AArch64 executable into a Lean semantics of the instruction set, and has agents prove forward secrecy and post-compromise security about the binary, in about 6.5 million lines of machine-checked proof resting on about 26,000 trusted lines; Part 3 sets it beside Theorem's result. The trade-off is volume. The proofs are enormous and bit-level, but each step has a simple shape that a model can grind through.

Read across the five routes and the pattern is consistent: the more of the translation a deterministic tool does, the more the AI is confined to specification and proof, which is where it is useful and where its mistakes are caught. Part 3 returns to the five routes side by side.

04 Where AI Earns Its Keep

The evidence points to four places where language models change the economics of verification. In all four, the model proposes and a symbolic tool disposes.

Falsifying Before Proving

The most expensive way to waste AI compute is to ask a prover to prove something false. Lean does not announce that a goal is false; the search agent expands subtrees and calls solvers until its budget runs out. Pipelines do well when they put cheap falsifiers in front of the prover.

LeetProof does this at the specification level. Before any code exists, the model drafts a Lean pre- and postcondition and about ten test cases, and Plausible checks three things: that every test input satisfies the precondition, that every intended input-output pair satisfies the postcondition, and, by mutating expected outputs (flipping booleans, nudging integers, dropping list elements), that no wrong output also satisfies it. That third check catches the classic underspecified postcondition in milliseconds.

Run against the human-written reference specifications of two published Lean benchmarks, the same harness found defects in roughly a tenth of them, on a laptop, in minutes. The seL4 work of He et al. does the same inside tree search, running QuickCheck and Nitpick on each new subgoal and pruning any branch that admits a counterexample.

Decomposing Hard Goals

Early neural provers predicted one tactic at a time, which works for five-step lemmas and loses the thread over fifty. Modern systems, from Draft, Sketch, and Prove to Goedel-Code-Prover and Aristotle, separate planning from discharge. The model splits a hard goal into intermediate lemmas left as sorry; the kernel checks that the skeleton is valid modulo those holes; and workers attack each hole in parallel, decomposing again where they stall. The kernel's check of the skeleton is what makes this safe to parallelize.

Guessing Invariants

For fifty years the hardest step in automating verification has been inventing an inductive invariant: a property that holds on loop entry, is preserved by the body, and is strong enough at exit to imply the postcondition. Symbolic techniques, from abstract interpretation over polyhedra to interpolation, IC3/PDR, and ICE learning, work bottom-up over formulas and choke on nonlinear relations or properties that are obvious to a human reading a variable called sorted_prefix_len.

Models have the complementary strength. Lemur, from Wu et al., made the division of labor precise: the model is an untrusted oracle that proposes properties and repairs them, and a sound verifier checks both that each proposal implies the goal and that the program actually establishes it. Nothing the model says is believed until it is checked. The same pattern drives Laurel for Dafny, Clause2Inv, and the invariant stage of LeetProof, and it works even with small local models wrapped in a counterexample loop.

Repairing From Diagnostics

Finally, models are good at turning type errors, failed goals, and model-checker counterexamples into fixes. VeCoGen, from Scania and KTH, pairs a model with Frama-C's WP and RTE plugins to refine ACSL annotations and C code, and reports fully verified C for 13 of 15 competitive-programming problems. Forge's single-pass generation converged in zero of thirty runs; with verifier feedback, all fifteen runs in a separate set converged within two or three iterations.

The same loop works for Rust. Microsoft's AutoVerus drafts, refines, and debugs Verus proofs and closes more than 90% of a 150-task benchmark, many in under half a minute, and SAFE bootstraps a Verus prover by verifying thousands of real Rust functions. Set against the vericoding result, that suggests Verus's low score there is more a synthesis problem than a proof problem: AutoVerus proves code that already exists, while vericoding asks the model to write the implementation as well. The upstream problem is getting existing C into safe Rust, which has its own pipeline; see Automating C to Safe Rust Translation.

05 Seven Ways AI Verification Fails

If the loops work this well, why can't we point an agent at OpenSSL or a 100,000-line Rust service and collect a Lean proof tomorrow? AlphaProof Code comes close for libsignal, and it still took a team of five four weeks, most of it spent on specifications. The failure logs across seL4, LeetProof, CLEVER, DafnyComp, and production Rust and C extraction show seven structural failure modes. They are taken here in the order a pipeline meets them: getting the code into Lean, searching for the proof, composing proofs across functions, and finally the specification and the world the proof is about.

Termination, Partiality, and Dependent Types

Three traps recur when general-purpose code meets Lean's logic. The first is partial def. Lean requires every ordinary definition to terminate, otherwise def loop : False := loop would prove anything. When a translated parser loop does not pass the termination checker, models trained on GitHub Lean reach for partial, which compiles and makes the function opaque to the logic. Nothing nontrivial can then be proved about it, and agents burn hours trying to unfold it.

The second is dependent indexing. arr[i] in Lean carries a proof that i < arr.size, so rewriting i to j + 1 changes the type of that proof, and Lean answers with the error every Lean user knows:

error: tactic 'rewrite' failed, motive is not type correct

The third is integers. Models biased toward Mathlib map uint64_t and size_t to Nat, where subtraction truncates (0 - 1 = 0), silently changing the meaning of high - 1. Keeping machine types instead introduces wrap-around everywhere, and bridging BitVec 64 reasoning to Mathlib's algebra requires cast lemmas where proof search routinely stalls.

Aliasing and Opaque Boundaries

Intrusive linked lists, parent pointers, Rc<RefCell<T>>, type punning a byte buffer into a header struct, lock-free ring buffers with acquire/release orderings: none of it fits a pure tree. Route B stops at the extraction boundary. Route D can model a flat byte array and interleavings, but then every write must be proved not to alias every invariant it might break, and the verification conditions explode.

Hallucinated Premises

Mathematics mostly lives in one heavily pre-trained library. Systems verification lives in thousands of project-specific types, accessors, and lemmas the model has never seen, and its proofs are procedural. Look at a script a model produced and ask what the goal looks like after wp runs:

apply hoare_seq_ext
· wp; simp [set_cap_def]
· wp; auto

Neither the script nor the text says what the goal looks like, and the first lemma is a hallucination: the library has no hoare_seq_ext. The meaning is in the prover's state. Figure 7 shows where the failed steps went.

He et al. analyzed millions of step-level tactic attempts on 241 seL4 theorems their system failed to prove, and the error taxonomy is lopsided: 60.1% of failed steps referenced a fact that does not exist, and another 17.9% applied a tactic that did not fit the goal's shape.

Standard retrieval does not fix this, because for a new module the analogous proofs do not exist yet and embedding retrievers do not match the shape of a procedural goal. What moved the needle was symbolic repair: use Isabelle's MePo relevance filter to pick the 128 most relevant local facts, and replace a hallucinated lemma name with its nearest real neighbors by edit distance. With that and counterexample pruning, the system proved 77.6% of the still-valid seL4 theorems it was evaluated on, where fine-tuned baselines on the earlier FVEL benchmark managed under 10%.

Retrieval does help when a project already has neighbors: Rango proves about 47% more Rocq theorems by pulling in similar proofs from the same project, which is exactly what a brand-new module lacks.

Late-Search Collapse

The common assumption is that models fail at the start of a proof. He et al. found the opposite: only 3.7% of failed seL4 runs stalled by depth 10. Most made real progress, unfolding definitions, running wp, splitting cases, and then collapsed late. By step fifteen the goal has dozens of hypotheses and a forty-line conclusion; the model's likelihood ranking no longer separates a step that simplifies an invariant from one that merely shuffles terms; and the leaves mix record updates with nonlinear arithmetic that neither Sledgehammer nor grind closes in one leap.

Composition Collapses

Most verification benchmarks, VERINA, VeriBench, DafnyBench and the rest, are single functions. Real software is a call graph. DafnyComp measured what happens when success depends on reasoning across function boundaries: verification fell to about 3.7%, far below the 58–68% the same paper reports on single-function Dafny benchmarks such as DafnyBench. The models still wrote syntactically valid Dafny almost every time; what failed was the proof. Figure 8 compares the syntax-correct and verified rates.

Two mechanisms explain it. If f calls g and the model wrote a postcondition for g that is true but too weak, g verifies and the proof of f stalls twenty minutes later. A human backtracks and strengthens the contract; current agents spin inside f. And in stateful embeddings every call must prove frame conditions over every field it did not touch, so the goal grows with the depth of the call graph. AlphaProof Code assigns that job to dedicated roles: an architect agent designs and periodically revises the decomposition of the proof, and an integrator merges proved lemmas and generalizes them for reuse.

Certifiably Wrong

Suppose an agent hands back a Lean file with zero errors and zero sorry. Is it correct?

Kleppmann, Vadim Zaliva, and the LeetProof authors all make the same point: once proofs are cheap, the specification is the single point of failure.

A system proved against a bad specification is simply wrong with a certificate. Agents that can edit the specification find the loopholes:

• Vacuous preconditions. Strengthen Pre until it is contradictory (n > 0 and n = 0) and the kernel accepts a one-line proof of a theorem that covers no inputs.
• Underspecified postconditions. Specify that sort returns an ordered array, forget to say it is a permutation of the input, and returning [] is fully verified.
• Defective benchmarks. The LeetProof team found 16 defective reference specifications in VERINA (15 since fixed by its authors) and 18 in CLEVER, mostly underspecified postconditions, written by humans and peer-reviewed. A 2026 agentic audit went further, flagging arguably wrong reference specifications in 80 of 161 CLEVER entries.
• Loopholes in the checker. The AI-assisted Collatz "disproof" described earlier found its loophole inside the Lean kernel rather than in a specification.
• Specification cost. Datadog engineers building with agents behind verification harnesses estimated, informally rather than by measurement, that the mental overhead of writing specifications and invariants is roughly two to three times that of writing the code.

The benchmark audit is the part that stings. When LeetProof's generated specifications were compared with VERINA's references, the human-written side carried more defects than the model's. Figure 9 shows the defect counts.

The World Outside the Model

Even a complete, non-vacuous proof is about a model. As Andrew Dickson argues, proofs live in closed symbol systems while software runs in an open physical world: a proof does not stop a sensor from icing over or a DRAM row from flipping. And there is operational friction. Sending proprietary source to a cloud model may break confidentiality rules; silent model updates break the reproducibility that certification regimes such as DO-178C expect; and $5 to $500 of test-time compute per function per commit does not scale to a repository.

06 Four Architectures Worth Copying

The research systems that do best arrange the loop between humans, models, and symbolic tools around those failure modes. Four are worth studying.

A: Mode-Aware Staging (LeetProof)

Earlier pipelines such as Clover and Laurel used one verifier and one mode, so an SMT timeout was the end. LeetProof matches each stage to the cheapest mode that can falsify or discharge it: specification inference checked by mutation testing, imperative Velvet code and invariants checked by #guard and Plausible (with a judge that rejects attempts to sidestep the imperative code with pure Lean), then VC generation and SMT, a recursive decomposition agent with Mathlib search, and Aristotle for the hardest leftovers.

On VERINA its generated specifications were judged semantically accurate in 97.4% of 188 cases: 150 strictly equivalent, 16 where the reference itself was buggy, 14 sound precondition variations, and 3 ambiguous but defensible descriptions. The other five were three incorrect specifications and two over-restrictive but sound ones.

B: Search With Premise Repair (He et al.)

Where LeetProof synthesizes small programs from scratch, He et al. prove theorems inside a huge existing proof base. Their loop fine-tunes an open-weight model on state-step pairs from an Isabelle REPL, repairs failed steps by relevance filtering and edit distance rather than regenerating, prunes children that QuickCheck or Nitpick refute, ranks survivors by likelihood, and calls Sledgehammer at stalled leaves. That combination is what reached 77.6% coverage of the seL4 theorems.

C: A Human-Reviewed Middle Layer (Zaliva)

The first two architectures skip a question: however the code and proof are produced, how do we know they match what a human meant? There is no algorithm for that, a limit Shuvendu Lahiri has stressed in his work on evaluating how well models formalize user intent.

Asking humans to review raw generated code, or fifty thousand lines of generated Lean, is a category error. The alternative is to make the specification the thing humans review. nl2spec, from Cosler et al., translates natural-language requirements into temporal logic interactively, showing the user each sub-translation so that an ambiguity is resolved by a person rather than guessed by the model.

A 2026 preprint by Vadim Zaliva pushes the idea into a whole pipeline: ground both code synthesis and proof in one shared intermediate specification that a human reviews, written with templated requirement languages and controlled natural language with certified parsing in Lean. Once that layer is agreed, the implementation can be generated in a proof-friendly language rather than C.

D: Model-Driven Repair (Forge)

Regulated industries cannot abandon Java or C without invalidating their certification evidence. Forge keeps the language and constrains it: the model writes Java in an extraction-friendly profile, deterministic transformations produce Dafny, CSP, and Isabelle artifacts, and any failure flows back as a structured repair prompt. The repair loop is what took it from no converged runs to all of them, and the Isabelle phase was consistently the wall-clock bottleneck.