Lean creator says AI made formal verification viable for everyday dev work
- Reading
- 6 min
- Tables
- 1
In an interview with The Data Exchange podcast, Leo de Moura, creator of Lean and VP at AWS, explains how AI models now translate code from any language into machine-checked mathematical proofs, from compression libraries to cryptography libraries.
The bottleneck is no longer generating code, it's trusting it
In an interview with the The Data Exchange podcast, hosted by Ben Lorica, Leo de Moura (creator of Lean, VP and Distinguished Scientist at AWS, and Chief Architect at the Lean Focused Research Organization) describes a scenario that changes the bar for anyone writing AI-assisted software: generating code has become easy, but proving it's correct remains the real problem.
Lean is both a programming language and a proof assistant. In it, you can write code and, alongside it, state the properties that code should have, backed by machine-checked mathematical proofs. The part that needs to be trusted is small: the kernel that checks the proof. Everything else, LSP, autocomplete, code generation, is just support.
Testing is great for showing the presence of bugs, but not their absence.
Leo de Moura, creator of Lean and VP Distinguished Scientist at AWS
The difference between testing and proving
The distinction de Moura draws between traditional QA and formal verification helps explain why one doesn't replace the other.
| Automated tests | Formal verification (Lean) | |
|---|---|---|
| What it guarantees | That the tested cases work | That EVERY possible input works, with mathematical proof |
| What it finds | Presence of bugs | Absence of bugs, when the proof holds |
| Historical cost | Low and easy to scale | High, but drastically reduced by AI agents, according to de Moura |
According to him, the two techniques are complementary, not competing: it's worth testing first to build confidence and understanding of the problem, and only then moving on to the proof, which covers any possible input instead of just the cases the team thought of.
From automatic translation to the 2.5-million-line Mathlib
The leap de Moura credits to AI has a name: autoformalization, the ability of a model to read a text (a math paper, or code in any language) and translate it into Lean on its own.
I mean, if someone had told me this last year, I would have said this is science fiction.
The example he uses to size up the leap is Mathlib, Lean's human-maintained math library: 2.5 million lines built over ten years. Today there are already published AI-written proofs with 50 million lines, and the proof of Fermat's Last Theorem, written by an Anthropic system, has 13 million lines.
Verifying real code: zlib, Rust, and Microsoft's SymCrypt
To move beyond pure mathematics, de Moura cites an experiment by a colleague, Kim Morrison: she ported the zlib compression library to Lean and formally proved that compressing and then decompressing data always returns the original data, lossless, at any compression level.
For those who code in Rust, there's a more direct path: the Aeneas tool makes it possible to verify Rust code using Lean without rewriting the entire project in the language. According to de Moura, Microsoft's SymCrypt team (the company's cryptographic library) already uses Aeneas combined with Lean to verify its own cryptography library.
The other alternative, newer and more generic, is to ask the AI to build a model in Lean from code in any language, without a dedicated tool. The risk built into this approach, which de Moura himself highlights, is that the generated model might not be faithful to the original code, hence the adoption of differential testing: running the real program and the Lean model side by side, comparing outputs to find discrepancies.
The Claude Code case: an agent finding bugs without its owner knowing Lean
The most concrete example of practical use came from within Anthropic itself. According to de Moura's account, Boris, lead developer of Claude Code, published a video in which he asked Claude to check Claude Code itself for bugs using Lean.
The agent created models of the code, tried to prove properties, identified where the proof didn't hold, isolated real bugs, and opened pull requests, which Boris accepted and merged. Boris, according to the account, doesn't know Lean.
In short: the practical gain here isn't the dev becoming a mathematician, it's the AI agent using formal proof as a bug detector more rigorous than a test suite, even without the human understanding the details of the proof.
Where trust can still break down
Not everything is automatic gain. De Moura uses the controversy surrounding the proof of the Navier-Stokes equations, attributed to OpenAI, to show where the process still falls short: the informal version of the proof, in natural language, and the formal version in Lean had a subtle divergence over the order of a derivative (fourth versus fifth), which matters to mathematicians even though it's a small technical detail.
The cause, according to him, isn't a failure of autoformalization itself, since the problem statement had already been validated by specialists before AI even entered the picture, but the lack of a tool that kept the natural-language version and the Lean version automatically aligned. He cites Verso Blueprint, a literate-programming-style tool that mixes natural language, LaTeX, and Lean, as the kind of tooling that would have avoided this mismatch.
Another point he emphasizes: a Lean proof isn't a static object. It can be refactored, simplified, and reduced, the same way code is refactored, always with the kernel confirming the proof remains valid after the change. Independent groups have already cut the proof of Fermat's Last Theorem in half.
Who checks the kernel that checks everything
An obvious question remains: if everything depends on the Lean kernel, what guarantees the kernel itself is correct? De Moura answers that the project doesn't rely on trusting his team alone: there are multiple independent kernels, some already formally verified, implemented in Rust, C#, Haskell, and, curiously, even in TeX.
These kernels compete against each other on speed and correctness at arena.lean-lang.org, publicly: a kernel that gets something wrong is penalized and it's visible for anyone to check.
What changes for developers in Brazil
The direct takeaway for those developing software in Brazil is that formal verification has stopped being an academic niche restricted to critical systems (avionics, security protocols) and has become a tool that an ordinary team can tap into via an AI agent, without needing to learn Lean from scratch, as in the Claude Code case.
This doesn't eliminate the engineer's work, it just shifts where they spend their time: instead of reviewing line by line, the effort goes into writing the right specification (what the code should guarantee) and systematically questioning whether the AI-generated model is truly faithful to the code in production. De Moura sums up this shift by comparing proofs to a safety net for aggressive AI optimizations:
It's almost like the proofs are guardrails.
For Brazilian projects dealing with sensitive code (payments, cryptography, infrastructure), the path described by de Moura, Aeneas for those already working in Rust, or an AI-generated model with differential testing for other languages, is technically viable today without rewriting the system from scratch. What remains open, by his own account, is the maturity of the tools for keeping the formal specification and the real code always in sync as the project evolves.
Translated from the Brazilian Portuguese original · Read the original
AWS Has Reserved Capacity Sold Out Through 2027, But Sets Aside a Share for On-Demand Use
Andy Jassy confirms that large blocks of AWS capacity are largely sold out through 2027, with part of 2028 already allocated. The company says it keeps room for on-demand EC2 and Bedrock, but developers are already reporting queues for common instances.
