"The tests pass" and "the code is verified" are not the same claim. The first says no failure appeared in the inputs we tried. The second says a property holds for every input allowed by a specification. If the specification is wrong, a correct proof can still preserve the wrong behavior.
Leonardo de Moura, the creator of Lean, explores that gap in a Data Exchange interview. The page carries both October 29 and October 21 dates, so this article treats it as a late-October conversation rather than asserting a single publication date. The analysis below draws on the transcript and public Lean material. We did not install Lean or compile the example.
Testing and proof are complements
De Moura's distinction is simple. Testing can reveal the presence of bugs, not their absence. A formal proof can show that a specification holds for all allowed inputs. The proof is only as meaningful as the specification.
He also gives testing its due. Writing tests improves understanding and can expose a false assumption before anyone attempts a proof. A specification that is already false cannot be proved no matter how many tokens are spent.
The zlib example in the interview makes the difference concrete. A theorem states that decompressing compressed data returns the original, under stated conditions, and a general-purpose AI produced the proof. The important part is not that the library was tested. It is that the round-trip property was written down as a machine-checkable claim.
Three gaps that appear when AI seems to understand code
The interview describes AI translating code from another language into a Lean model and using that model to find bugs. One anecdote involves Claude Code's developer asking an agent to model the code in Lean; the resulting bug reports led to real fixes. That is useful for bug finding, but it is not the same as establishing the absence of bugs.
| Gap | Question | Failure mode |
|---|---|---|
| Requirements | Did we write down what we actually want? | The code satisfies the spec but not the user's need |
| Model fidelity | Does the Lean model behave like the real implementation? | A proof about the model says nothing about the shipped code |
| Kernel and trusted base | Which checker and assumptions do we trust? | Checker bugs, library assumptions, unintended axioms |
De Moura mentions a similar problem in the Navier-Stokes case. The informal proof and the Lean proof diverged on a subtle assumption, such as the derivative order. That can change the mathematical meaning while still looking like the same theorem from a distance.
These gaps matter more in the agent era. As generation becomes cheaper, what remains is deciding what must hold and who checked it with which tool.
A weak specification can still be "proved"
Here are two Lean 4-style specifications. This is explanatory code, not a compiled or verified example. The sorry in the second theorem is a placeholder, not a proof.
def clamp (x lo hi : Int) : Int := max lo (min hi x)
-- Weak: only says that some integer is returned.
theorem clamp_returns_a_value (x lo hi : Int) :
∃ y, clamp x lo hi = y := ⟨_, rfl⟩
-- Meaningful: when lo ≤ hi, the result stays within both bounds.
theorem clamp_bounded (x lo hi : Int) (h : lo ≤ hi) :
lo ≤ clamp x lo hi ∧ clamp x lo hi ≤ hi := by
sorry
The first theorem is true but nearly vacuous. The type already says the function returns an integer. Proving it and then announcing that the code is "formally verified" reproduces the problem de Moura describes: a property that is effectively no property at all.
The second theorem constrains the result. Its precondition, lo ≤ hi, is part of the requirement too; without it the statement may be false. A useful specification also makes clear what it does not guarantee.
Questions for a verification claim
De Moura's advice to a buyer is direct: show me the specifications. Ask which properties were verified, which checker was used, and what the trusted base is. In practice, that becomes a checklist.
| Question | A useful answer | A warning sign |
|---|---|---|
| Which properties were proved? | Theorems, invariants, preconditions and exceptions are public | Only "the code is verified" |
| How does the spec map to requirements? | Traceability and review records | A list of test names |
| Why does the model match the implementation? | Extraction, translation tooling, differential tests, manual review | "The AI wrote the model, so it matches" |
| Which kernel and trusted base? | Independent checkers, small trusted base, version information | Checker details withheld |
| Are failure paths specified? | Error returns, resource exhaustion, concurrency conditions | Only the happy path |
| What does maintenance cost? | Spec change process and re-verification time | "Prove it once and you are done" |
Lean offers tools for some of these answers, including multiple proof checkers and Aeneas for verifying Rust code through Lean. Tooling does not automatically make the specification correct or keep the model synchronized with the implementation. Those remain engineering work.
A practical sequence for AI-generated code
Not every project needs formal verification. De Moura also notes that different software warrants different levels of assurance. Start where failure is expensive and the property is stable.
- Pick one critical invariant. For example: "retrying a payment never charges twice" or "an unauthorised user cannot read this data."
- Express it as an executable property test first. Keep the generator and the smallest failing case.
- Check model-to-code fidelity. Use differential tests or an extraction path that connects the model to the implementation.
- Move to proof only when the specification is stable and failure is costly. Prototype UIs and rapidly changing product requirements may be better served by tests and review.
- Document the claim. Record which property was checked, with which tool, under which assumptions.
AI can shorten this work. It can draft a Lean model, search for counterexamples, or sharpen a specification. It cannot take responsibility for the two human judgments: whether the model matches the code, and whether the specification captures what users need.
The interview's conclusion is less about the end of coding than about where responsibility moves. AI can write more of the code, but someone still has to decide what must be guaranteed and leave that guarantee in a checkable form. As code gets cheaper, the ability to own a specification becomes more valuable.
This is an interpretation of published concepts, not a measurement of Lean adoption or product performance. The Lean example was not compiled.