When AI Writes the Code, Who Proves It Works?

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.

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 Jump to transcript Related content: 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. Leo de Moura.

Yes.

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— Ben Lorica. No matter what language. 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. Leo de Moura.

Yes.

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— Leo de Moura.

Yes. Ben Lorica.

As recently as maybe a year ago, it’s now a thing. Leo de Moura. Exactly, exactly. 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. Leo de Moura.

Yes.

Ben Lorica. The frontier models are now capable of translating whatever program you wrote, in whatever programming language, into Lean. Leo de Moura.

Yes.

Ben Lorica. And then now you have the Lean infrastructure for verification. Leo de Moura.

Exactly.