AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura

I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated code and a human only needs to ensure that the generator provably generates the correct mass scale assertions.

This is how formal methods can constrain AI for large systems.

We're doing this at the Open Markets Initiative, where we've generated millions of lines of Lean 4, TLA+, and Rocq that ensure that our open source electronic trading protocol code is accurate. We didn't expect it but the Lean prover did identify some incorrect steps. https://github.com/Open-Markets-Initiative

What do people think of property based testing? I’ve set up a few property based tests and it feels almost like formal verification.

I know it’s not the same thing, but PBT’s can catch all sorts of absolutely crazy bugs that I never would think to check for. Stateful stuff, cross-service stuff. My only gripe with PBTs has always been the tedious setup, but LLMs solve that.

I haven’t seen much discussion around PBTs lately, but you get a ton of bang for your buck in the LLM age

> ... 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.

Does anyone have resources on learning modelling for formal verification? (Does not have to be in Lean)

If you use agents to generate formal verification, how do you tell if the properties that are verified are the correct ones?

Currently the foundation theories in mathlib are built with the assumption that formal proofs are expensive. Concepts are fragmented to share as much proof as possible. With LLM the assumption is no longer correct. Concepts and proofs should be built to fit human thinking as much as possible and proofs can be ported by LLMs between theories. Lean would ensure that the translation is correct.

I just don’t know why we are using a verification that is hard to read and write for humans

I guess I'm missing something but I don't see how this isn't just:

1. Creating more work 2. Shifting the existing work to specification

There's not really such a thing as a perfect specification. One of the things AI is taking away is character by character feedback cycles. Can't count how many times I'll be writing software and think in the middle of writing a return, realize this is probably not what I should be doing. I'm not sure how you would really replicate that experience when creating specs... nobody is going to sit and meditate on their specs for hours before writing them.

Examples of comparing the results of Lean and e.g. Rust as is described in the video?

I have symbolic error terms in Lean that I guess can be sampled and compared to Monte Carlo analysis? But I already had sampling-based analysis, that's why I had to do all of this (double-slit experiment and gravity with GrC(2,4)) in Lean 4.

What would it take to combine Lean and one or more Rust TLA+ implementations? How does an agent plan and implement this and what are the advantages and disadvantages?

"Comparison of Isabelle/HOL, Lean, HOL4, and Agda: A Tale of Four Theorem Provers" (2026) but not Rocq? https://news.ycombinator.com/item?id=50043202

[flagged]

[dead]

[dead]

[flagged]

[flagged]

... somewhat disappointed the guy is now associated with AWS. I guess I was hoping for a non-profit organization.

While learning and applying formal verification in the context of using AI agents, what I feel is that sometimes it's hard to express my own thoughts as formal verification. But more than that, I doubt whether formal verification being done correctly actually solves the phenomenon of AI spinning in circles on a specific task.

For example, I want to eat chicken, so I try formally verifying "chicken dish," and every time GPT or Claude starts digging into the origin of the sauce in the chicken dish or the breed of the chicken. Then the chicken dish never gets finished and never makes it to dinner, and instead I gain deep knowledge about the origin of chickens.

Of course, I know that formal verification has liveness — meaning that there must be progress in the work is also part of formal verification — but the AI judges that learning the origin of the chicken counts as progress too. Yet it ends up doing work that it actually shouldn't be doing.

Personally, while organizing these AI anti-patterns, I feel that when you formally verify one condition, verification of another condition gets weakened, and within that phenomenon I sense the AI spinning in circles again. In the end, I end up going through the process of reading and merging everything one by one myself, and I want to know whether this is something only I experience.

I noticed a problem in the "AI is our future!" crowd.

What they do, does not really interest me. With that I mean it is nice that they can solve many problems as-is, and that will probably become more important - but I am just not interested in looking at AI project. It is totally meaningless to me.

In the past, when you, say, have a project written by a real human author on github, this could be interesting. With AI generated projects, I just don't have the slightest interest in "connecting". I also don't think to be the only one; you notice this on youtube too. Some people no longer have an interest in AI-generated videos and avoid them. I am curious when the AI hype phase will go down; right now it seems to not come down but I think it eventually will.