Leo de Moura on Formal Proofs, AI Agents, and the End of “Trust Me” Code.
Subscribe: Apple • Spotify • Overcast • Pocket Casts • YouTube • AntennaPod • Podcast Addict • Amazon • RSS .
Ben Lorica speaks with Leo de Moura , creator of Lean , VP and Distinguished Scientist at AWS , and Chief Architect of the Lean Focused Research Organization , about how AI is making formal verification more accessible and potentially transforming software engineering. They discuss the growing importance of specifications and machine-checked proofs, what it means to trust AI-generated code and autonomous agents, and the vision of a verified software stack. The conversation also explores how AI and formal verification are reshaping mathematics, what this means for the skills and careers of engineers and researchers, and where similar breakthroughs might emerge next.
Subscribe to the Gradient Flow Newsletter
Interview highlights – key sections from the video version:
Introduction to Leo de Moura and Lean
Why AI-Generated Code Needs Formal Verification
Verifying Rust, Autoformalization, and Scaling Mathlib
Can AI-Generated Formal Models Be Trusted?
Navier-Stokes, Proof Mismatches, and Editable Proofs
Formal Verification vs. Traditional Software Testing
How AI Is Making Formal Verification Practical
Requirement Gaps, Model Gaps, and Trusting Proof Checkers
The Future of Software Engineering: From Code to Specifications
The Verified Software Stack and Evaluating Verification Claims
Verifying AI Agents, Sandboxes, and Security Policies
Mathlib, AI-Assisted Mathematics, and Collaborative Proofs
Can AI and Formal Verification Transform Theoretical Physics?
The Future of Mathematicians, AI Compute, and Scientific Discovery
Beyond Mathematics: Finance, Chemistry, Accounting, and Law
A video version of this conversation is available on our YouTube channel .
How AI Is Changing Mathematical Research
Passing Your Evals Doesn’t Mean You’re Safe
Eight Security Assumptions AI Agents Quietly Break
Nine Practical Rules for Agents Doing Real Work
Zhou Yu → Why Your AI Agent Isn’t Ready to Ship (And How to Know When It Is)
Helen Gu → The Hidden Failure Modes of AI Agents
Evan Marshall → As Code Generation Speeds Up, Who Tests the Output?
Support our work by subscribing to our newsletter📩
Transcript
Below is a polished and edited transcript .
Ben Lorica. All right. So today we have a treat. We have Leo de Moura, VP and Distinguished Scientist in the Automated Reasoning Group at AWS. More importantly, he is the creator of Lean, which can be found at lean-lang.org. Lean is both a programming language and a theorem prover, and he is also the Chief Architect of the Lean Focused Research Organization. So, with that long-winded introduction, Leo, welcome to the podcast.
Leo de Moura. Thank you, thank you. Very excited to be here.
Ben Lorica. All right. So, I guess the overarching thesis of this conversation is that we’re in an era where generation has become easy. Not necessarily cheap, as people who use Claude Code will attest, but easy. And so, one of the key challenges is verification. Lean is normally associated as the go-to tool. In fact, I think it’s going to be a tool that will increasingly be on the lips of many people in AI in the next year, around the topic of formal verification. So I guess let’s start here, Leo. Just the basics: for a listener who’s accustomed to code reviews, QA, and testing, what does formal verification mean?
Leo de Moura. Yeah, Lean is both a programming language and a proof assistant, right? You can write code, but also state properties the code should have. You can state open conjectures in math, and you can provide proofs of these claims, right? But the proof is not informal. The proof is written in the Lean language, and more importantly, it’s machine-checked.
Lean is a big piece of code, but to trust a result proved with Lean, you need to trust only the kernel, right? That’s where the proof is being checked. Like any other programming language, you have all the tooling: LSP server, IntelliSense, code generators, autocompletion. All these features are available in Lean, but they’re not important for the proof-checking step.
And we have more than one checker. In Lean, you can view proofs as data that can be manipulated, that can be transformed. You can export your proofs and check them with different checkers. Some of these checkers are verified now. We have two verified checkers. A third is coming soon.
But this ability to have machine-checkable proofs helps address a trust bottleneck, not just a trust bottleneck between humans, but also between humans and AI.
For example, suppose you want to synthesize a piece of code. You want to implement a piece of code that has specific properties. In the past, you would implement the software. Maybe you would add some testing infrastructure to make sure these properties hold. Property-based testing is very popular these days, right? And you would write the testing framework.
The testing framework is very useful for finding bugs, right? But it’s not useful for proving that there are no bugs.
Ben Lorica. You may even have a separate team conduct the testing.
Leo de Moura. Yes, yes. Now, with formal verification, you can start with the properties. You can, for example, write the properties down and ask the AI to implement a piece of code that satisfies these properties, and prove it to me. You’re going to implement the code and write a proof, a Lean proof, that will be machine-checked. And AI now is fully capable of doing that.
For example, a colleague and friend of mine, Kim Morrison, did an experiment where she ported zlib to Lean. This is a compression library. And now she has a property that says that if you compress data and then decompress it, you get the data back. There is no loss. The data was not corrupted. It’s an important property.
Ben Lorica. No matter the level of compression.
Leo de Moura. Exactly, exactly, exactly. Great, great. The theorem says exactly that. It’s one of the parameters of the theorem.
Ben Lorica. And so, Leo, for our listeners, she did this. She wrote this compression tool using Lean.
Ben Lorica. And then Lean served as kind of the formal verification tool. So if I’m a developer and I do the same thing, and I say I’m going to use Lean to formally verify my software, but I’m going to write it in Rust first, can Lean still help me?
Leo de Moura. Yes, yes, it can, in two different ways. The first way is using Aeneas. Aeneas is a tool that allows you to verify Rust code using Lean.
Aeneas is used, for example, by the SymCrypt team at Microsoft. SymCrypt is the cryptographic library at Microsoft. They use Aeneas plus Lean to verify the crypto library.
So you can start by using Aeneas. Another possibility is to ask your AI to build a model of your code in Lean. The AI will read your code, no matter—
Leo de Moura. Yes, no matter what language. I mean, if someone had told me this last year, I would have said this is science fiction.
Ben Lorica. And this has a name, at least in mathematics. They call it autoformalization.
Ben Lorica. Right. So, in mathematics, for our listeners, you might have a math paper, and it’s a paper, so it’s composed of words, mathematical symbols, theorems, lemmas, and so on and so forth. And then autoformalization, which, as Leo points out, was not a thing—
Ben Lorica. As recently as maybe a year ago, it’s now a thing.
Ben Lorica. And so, Leo, this step, you folks at Lean had nothing to do with. This just happened because the frontier models became capable of doing this.
Leo de Moura. Exactly, exactly. From the Lean side, what changes for us? Scalability, right? I mean, now AI—for example, the mathematical library built by humans for Lean is called Mathlib. It has 2.5 million lines.
Ben Lorica. Incredible! For our listeners, imagine—and this is not the case—but imagine almost all mathematical books and papers were translated, in the way we described using autoformalization, into Lean, which means then you have access to all of them.
Leo de Moura. Yes. But look at these speeds now. There are Lean proofs now that have been published that are 50 million lines. Mathlib took 10 years, written by humans, to go from zero to 2.5 million. And now there are people writing proofs—that’s AI writing the proofs—that are 50 million lines. The Fermat’s Last Theorem proof that was written by Anthropic AI is 13 million lines.
Ben Lorica. But in the case, as you point out, Leo, of software, there’s something equivalent going on for every programming language.
Ben Lorica. The frontier models are now capable of translating whatever program you wrote, in whatever programming language, into Lean.
Ben Lorica. And then now you have the Lean infrastructure for verification.
Leo de Moura. Exactly. But one important thing to keep in mind when you create a model of your program in Lean, if you use AI, there’s always this question: is this model faithful to your code?
Some people now are using differential testing, right? They run the Lean model and the program and see if they compute the same thing, right? To find discrepancies. And people have been finding bugs. I mean, even—
Ben Lorica. So what you’re saying is you’re still responsible for this.
Leo de Moura. Yes, exactly. And I see it happening in an incremental way. For example, a few weeks ago, the Claude Code main developer, Boris, posted a video where he just asked Claude, “Oh, check Claude Code for bugs using Lean.”
And Claude starts creating the models, finds bugs, tries to prove properties, notices that it cannot prove the properties, finds bugs, files the PRs, and Boris merges them. Yeah, these were real bugs. And Boris said, “I don’t even know Lean.”
Leo de Moura. But this is for bug finding. This works reasonably well. But for the next step, for you to say, “Yes, there are no bugs,” now you have to start looking at the model and saying, “Yes, this is an accurate model of my code, and I want to maintain them in sync.”
Maybe I will use AI. I will prove properties. You can start using Aeneas if your code is in Rust. You can try to use Aeneas to prove that it’s a faithful model of your code.
But we expect, in the next few months and years, people will focus way more on the specifications, on the models, on the properties you want the software to have.
Ben Lorica. So, yes. In fact, this same phenomenon is happening in math, most recently in this proof of the Navier-Stokes equation, right? So maybe the autoformalization step of translating the actual statement of the problem may not have been as faithful, or whatever.
But then it turns out that, in fact, they did prove the result. It’s just that, you know, you still needed humans to kind of catch this and make the subtle adjustments, right?
Leo de Moura. Yes. Yeah. No, this is an important point for Navier-Stokes, because it’s such an important result. Before OpenAI even started directing the models, we had a human-curated statement of the Navier-Stokes problem. The statement of the problem had already been curated by experts. There was no doubt about whether the statement of the problem was correctly formalized.
There’s some controversy in the results because OpenAI presented an informal proof written in natural language and a formal proof written in Lean. The informal proof and the formal one had mismatches in the proofs.
Ben Lorica. I think it’s at the level of whether you’re assuming a fourth or fifth derivative.
Ben Lorica. Which matters for mathematicians, but you can see how subtle the differences were, right? So, but Boris—but let’s give you—
Leo de Moura. Let me give you a point. There’s a tool that I think is important to tell your audience about. There’s a tool called Verso Blueprint.
Verso Blueprint is a tool for when you want to present a Lean result mixing natural language with Lean. You can use Verso Blueprint. It’s almost like literate programming. You can mix natural language, LaTeX, with Lean and align the two presentations.
We are very confident that if the AI was using Verso Blueprint, this mismatch would not have happened, right? I mean, this is a matter of improving the tooling.
Another misconception people have is that they think a Lean proof is a static object. It’s not. Like we refactor code, you can refactor proofs. You can simplify them. There are groups, for example, for the Fermat’s Last Theorem proof by Anthropic. There are groups that have already reduced the proof by half.
Ben Lorica. By the way, this is true for proofs written by humans too.
Leo de Moura. Yes, true. Yeah, yeah, yeah. But here you get the machine check, right? I mean, you’re modifying the proof, but Lean keeps saying, “Yes, it’s a true proof,” right?
You can manipulate it. You can ask the AI to help you navigate the proof. You can align the proof with the informal presentation using Lean blueprints. This is all possible, right?
I mean, this is one thing that I see on social media that people are missing. These formal proofs are not static objects. They’re objects that you can manipulate, you can simplify, you can probe, you can ask questions, you can interact with them.
Ben Lorica. So I guess I want to just nail down this one point, which I think should be clear by now. But I just want to make sure the audience, who may not be familiar with what we’re talking about, gets this point, which is this difference between formal verification and plain QA and testing.
Why do I need—I mean, why should I bother with formal verification when I already have AI writing all these tests for me? And, you know, because I’m using AI to generate a plethora of tests, edge cases, you know, I have maximum coverage. Leo, I don’t need verification, right?
Leo de Moura. Yeah, testing is great for showing the presence of bugs, but not their absence.
Even if you use the AI to generate many test cases, your AI may not be as smart as the AI that will be used to find a vulnerability in your software, right?
I think the technologies are not in conflict with each other. They complement each other. For example, one mistake I see many people making is trying to prove something that’s maybe buggy. Well, no matter how many resources you put into it, how many tokens you burn, you’ll not be able to prove something that’s not true, right?
So testing is always a great way to start, as it increases your confidence, your understanding, and then you prove.
Now you’re proving for any input. You’re not proving that only for the tests I tried, it worked. But you’re proving that for any possible input, your program works, right? It’s for all instead of for some, right?
Ben Lorica. And honestly, I think software engineering may be behind other engineering disciplines. I don’t know, like aerospace or whatever, right? So maybe they’ve had more rigorous discipline around verification because, after all, there are much more serious consequences in these other fields, right? So, great points.
Ben Lorica. I think this is just a case now that we have more and more people writing code, and code is easier to write. And it just happens that verification has had its ImageNet moment, so to speak.
I guess, Leo, the main thing that’s happened—because you folks have been working on Lean for a while, and Lean has been rock solid for a while—so the main transition is really this autoformalization, the capability of the frontier models to write Lean.
Leo de Moura. Yes, and it also connects to your previous comments. You made the point that, yeah, in some industries, people have used formal verification in the past. But why was it not popular, if it is so good? Because it’s too time-consuming to prove things by hand.
And AI dramatically reduces the cost of verifying code, and it gives you other benefits.
After you have a formal proof, right, you can start asking the AI, “I want you to change, optimize my code, but you have to keep proving that it is correct.”
It’s almost like the proofs are guardrails. Now the AI can try wild optimizations that you may not even understand exactly how they work, but you have a proof that’s saying, “Yes, it still computes the same thing.” It’s way more efficient, but it still computes the same thing.
Ben Lorica. So, based on what we’ve been discussing, it seems like the software engineering profession will now focus on not writing code. Maybe not even verification, because verification maybe you can also semi-automate based on what we’ve discussed.
It’s really requirements, right? So describing what you want.
So there’s two buckets, I guess. There’s the requirement gap. So is there a difference between what you want and what you are able to write down? And I guess what some people call the model gap, which is really: are the conditions around what you’re testing representative of production?
So, in other words, maybe your testing scenarios are too idealized in some ways.
And obviously, you alluded to this earlier: to some extent, you have to trust Leo and team, the Lean kernel, right? So as Lean becomes more popular, and you rely on it—and by relying, I mean you’re relying not only on Lean having verified your code, but all the libraries that your code depended on, right?
So I guess those are three things. There’s the requirement, there’s the model, and then there’s the Lean kernel.
Leo de Moura. Well, we have multiple. You don’t need to trust us. There are kernels implemented by other teams, right? This part, I think we’re addressing well.
I mean, we even have a kernel arena now where we collect kernels. They compete against each other to see which one is the fastest. If they get something wrong, if they have a bug, they are penalized, and everybody can see.
It’s called arena.lean-lang.org. You can see all of them. I mean, and all of them are—
Leo de Moura. I think so. I’m pretty sure. I mean, I cannot say, I don’t use all of them. I use the main ones. The ones I use, they’re all open source. I mean—
Ben Lorica. Do they have to be written in Lean to be—
Leo de Moura. Some of them are implemented in Rust. There’s one implemented in C#. There’s another one implemented in Haskell.
Believe it or not, there’s one implemented in TeX. TeX, people, is this language for typesetting math papers and papers in computer science, math, and so on. But TeX is a full-blown programming language, and a colleague of mine, Kim Morrison, implemented a checker, a kernel, in TeX just to show that you can implement it in many different programming languages.
Oh, there’s one in COBOL, for example, and one implemented in Fortran.
Ben Lorica. So then the education and training of a software engineer will change, right?
Leo de Moura. Well, I think there will be way more focus on writing formal specifications, writing properties. The requirements are essential.
Many times, we don’t even know exactly what the software is supposed to do, right?
Ben Lorica. And by the way, Leo, some of these applications are complex, right? So they interact with databases, distributed systems—
Ben Lorica. And so on. So then, I mean, how do you exactly—you’re not going to be able to nail down the requirements of—or maybe that’s what distinguishes