AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
thedataexchange.mediaI 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
Isn’t the point of TLA+ is to model aspects of design at such high level that no deterministic generation is practical as a rule. The TLA+ models may be useful for LLMs (help find real bugs).
Very Interesting!
Do you have a detailed paper/article written on this?
> 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 not completely clear; would you mind elaborating on that in more detail?
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
PBT testing and fuzzing are basically the same thing in my mind.
What's funny though is that the reasoning needed to say some sampling is comprehensive....makes it closer fo proofs! AFL — coverage-based fuzzing — was the original innovator here, but imagine an interpreter — code coverage in the interpreter itself isn't so good, you also want to explore the interpreted program!
This is why "is my testing comprehensive?" is actually an open-ended problem that, in the limit, is just as hard as formal verification.
I suspect we're basically going to see a convergence here. Randomized testing can be called "Monte Carlo formal verification" hehe.
> This is why "is my testing comprehensive?" is actually an open-ended problem that, in the limit, is just as hard as formal verification.
Well said! I learned about PBT in the first place because I watched a talk where the speaker referenced the story of foundationDB. Super interesting stuff. If anybody wants a link I can dig it up
I also think property based testing is great.
But they are very different IMO at what they focus on and so they occupy different places when talking about does a piece of software does what it should do and withing the state/parameters specified:
- Property based testing focuses on finding counter examples - Formal verification focuses to prove that a property always holds
More than this I think in all these discussions we are missing the most important piece: validation.
While verification means to prove or test or verify that the software does what is should do, validation means to prove or test or verify that the software is solving user needs.
So actually I've been testing this — it seems to be useful in limited cases. LLMs have gotten so good now that a properly defined spec is no worse than a spec + property based testing.
I still found it useful for
1. trusting a bit of code is correct
2. rule-dense bits of code (eg something like a date parser)
The real issue so far is that I'm having trouble finding tasks where an LLM can't correctly code up an exhaustively defined spec.
Property based testing is great because it’s implemented as a library in many languages. You don’t have to rewrite your codebase in Lean.
works really well for simulators, where you usually don't have an oracle but you do have invariants. e.g. in SPICE the low-freq AC gain has to match the slope of the DC sweep. it's cheap to check and it catches sign errors that look totally fine on a plot
Yeah, LLMs make setting up the annoying things like PBT and mutation testing easy. It’s great.
> ... 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)
Lamport’s book and or Hillel Wayne’s are both good. State machines as a specification language has always been pretty approachable and also relatively deep. If you want to get in to proof assistants Software Foundations is great and the delta to understanding Lean from Rocq is pretty small.
https://lamport.azurewebsites.net/tla/book.html https://logicforprogrammers.com/ https://softwarefoundations.cis.upenn.edu/
Mandatory Background:
1) Understanding Formal Methods by Jean-Francois Monin - This is the absolute best for getting a grip on the breadth, concepts and sample tools for Formal Mathematics/Specification/Verification. Fire-hose of information (not a step-by-step textbook) so use this as a map for everything "Formal". The S/N ratio is very high (~250 pages only!) so use AI/Textbooks to help explain concepts you find difficult to understand.
Practical:
1) Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - Uses "Alloy" language to teach Structural (i.e. Data) Modeling.
2) Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers by Leslie Lamport - Uses "TLA+" language to teach Behavioural (i.e. State Machine) modeling.
The above two are for "System Modeling" i.e. everything needed to formally build complete systems.
3) Finally, You should also look at the bunch of free books on the Lean4 website which can be studied parallely for "code-level" proofs and verification.
PS: There are a few more (eg. Event-B method etc.) but you can get to those if/when you need to.
Start here: https://github.com/bendlang/bend
This is a vibecoded project, not a resource for learning modeling for formal verification.
If you use agents to generate formal verification, how do you tell if the properties that are verified are the correct ones?
make no mistakes
mostly jk, although agents themselves are of course getting better at detecting whether a formal spec is faithful to a natural language spec
Applications: implications, simulations, and experiments. Gobble the frontier; wring out the usable.
This reads as gibberish.
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.
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
Nice article, here is the direct link since no one commented on the HN post.
A tale of four theorem provers - https://blueberrywren.dev/blog/primes/
> Broadly speaking, both Lean and Agda are dependent-types based systems, utilizing the Curry-Howard correspondence to prove theorems via a complex type system, whereas Isabelle/HOL and HOL4 are LCF-style systems, with a small "proof kernel" containing base rules (e.g. forall x, x = x) that all proofs must be constructed via.
In all my years of reading - and I've written my fair share of dangling prepositions - this is the first time seeing "via" at the end of a sentence. Let me guess the author is German, Danish, or a mathematician.
These abbreviations were not defined before use.
- LCF: Logic for Computable Functions - https://en.wikipedia.org/wiki/Logic_for_Computable_Functions
- HOL: Higher Order Logic - https://en.wikipedia.org/wiki/HOL_(proof_assistant)
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.
A sufficiently powerful agent with sufficiently long horizon task finishing ability will first invent the universe from scratch and only then will it finish your chicken dish.
I see not only me tried to give astra insufficiently described tasks
It seems you've summarized my problem properly. Haha.
You seem to be using "formal verification" with a non-standard meaning.
> I feel that when you formally verify one condition, verification of another condition gets weakened
In standard formal verification there is no problem here: you formally verify the composite "condition_1 AND condition_2"
The problem I often run into is this. It’s not formal verification, but I create a UML diagram to lay out the whole skeleton first. There are usually open-source architecture books, so I take it from there.
Then it should implement the whole UML skeleton, right? But it goes like this: halfway through, at some point, it says, “This algorithm is too slow? Hmm... I need to make it faster,” and tries local optimization, so sometimes I don’t get the result I want—that is, an MVP that at least runs.
I know the overall goal clearly, but there’s a problem where it gets obsessed with a specific subgoal or keeps expanding that subgoal.
Your problem is that you have not established "guardrails" for the AI and so it goes off and tries to do everything it can to help you (its default persona is "people pleaser").
AI understands "negative constraints" very well and so you should explicitly tell it "what not to do" at every stage as much as possible.
Use Top-Down and Stepwise-Refinement methodology to first generate the "Interface" and then the "Implementation" like so;
1) Ask it to produce only the "Skeleton App with well-defined Interfaces" directly 1:1 from the UML with stubs/mocks. It maybe better to use UML in text form which will allow you to annotate it easily with hints/notes for AI. The "Skeleton App" should include a) System Modules with narrow public interfaces like LKM/ioctl b) Directory structure with one module per subdirectory as a DAG with no cycles c) Explicit list of third-party libraries/frameworks to be used d) Classes/Abstract/Interfaces e) Free Functions and Class Methods with full type signatures etc.
2) Check the above and iterate until you have the UML and generated code synced up at the sufficient level of detail of Interfaces you are comfortable with. This should be compilable and is your absolute baseline which cannot be changed until you get a functional MVP.
3) Using the above skeleton, with strictly no change to any interfaces, ask it to fill in only the implementations the simplest possible way (i.e. "naive" linear, brute force etc.) with no optimizations whatsoever. Here you explicitly ask it to add runtime assertions for preconditions/postconditions/invariants. Make explicit that assertions should not have any side-effects whatsoever. This should now compile to give you the "naive" MVP.
4) Generate comprehensive test suites and test the above.
5) Now have it optimize everything, without changing the interfaces and assertions, but honouring them strictly. Compile and test against the above test suites. This should give you the "optimized" MVP.
6) Once the above passes, if performance is critical, have it comment out all assertions except "preconditions"; leave this in always. This is the minimal "sanity check".
7) Finally, for every "usecase" (i.e. feature) in the UML, have it generate the control flow graph annotated with preconditions/postconditions/invariants (which form the specification) from the previously generated code individually one per usecase. This is your "whitebox" verification documentation to make sure the implementation call graph satisfies the usecase i.e. feature specification.
Note that the above process gives you two implementations viz. the "naive" one and the "optimized" one. It is very helpful to always keep it that way as you modify/add features going forward so you can check one against the other.
You could use the same process using a textual Requirements Document etc. instead of UML. Also, if needed you can have AI generate the UML from the requirements, so you have a graphical specification of the system too.
This is the "Correctness-by-Construction" (CbC) approach using "Design-by-Contract" (DbC) methodology.
Additionally, If you generate for a strongly-typed language you can ask AI to explicitly exploit the type system fully with an eye to proving the code correct by suitable use of dependent types etc. to establish constraints for code correctness in step-1 itself as part of the interface. This is "Type-Driven Design". However, this is somewhat advanced and hence only do this if you have a good grasp of the implementation language since AI will try to be too clever and implement "typing hijinks" which can make the code incomprehensible.
Think of it as how you used wizards in older IDEs (Visual Studio MFC etc.) to first generate default skeleton app code with stubs/mocks, got it to compile and then started adding your code to it with testing and verifying at every stage. You want AI to behave in such a deterministic manner.
PS: To get started, feed my comment to AI and have it generate the necessary prompts for your AI interface ;-)
Can you try to get it to only specify interfaces first? Then tests, the write code to implement
I think my English is a bit lacking, so I didn't explain my situation well enough.
The main point is not that everything is solved if you specify all the conjunction conditions and prove that those conjunction conditions are correct. Rather, the key point is that in that process, the agent keeps expanding subgoals.
For example, two proofs, P1 and P2, are carried out, but they proceed in a way that diverges from the actual progress of the work. That is, you can prove things like "P1: the chicken is safe" and "P2: the origin of this sauce is trustworthy," but combining these does not make a chicken dish.
In other words, the proof logic holds, but my actual task doesn't get solved. I'm questioning how to solve this problem. It's frustrating that I'm not a native English speaker at times like this. I'm sorry for causing a misunderstanding.
For example, it goes like this.
I proved P1 and P2. But then it creates P1.1. It goes and finds information from an agency certifying that this chicken is safe, and puts that in. Then it starts creating P2.1 as well. The origin of this sauce is trustworthy, but maybe there’s a better one somewhere?
It goes on like that.
Ask the model to declare its assumed axioms. Agree that those can be trusted for the time being. Things like the behaviour of third party libraries. Ensure that your review agent enforces this.
Thanks for the advice. This is what I struggle with the most. I’ve learned formal verification other than Lean proofs and used it a few times. It holds up well, but as soon as it becomes a slightly longer-term task, it passes formal verification but turns into work that doesn’t reach the goal G I’m aiming for, and I don’t know how to solve that. I clearly need a separate review agent—have you built a separate harness for the review agent?
Other people say that when they do AI coding, they finish quickly, but for me it’s painful because I keep having to verify it myself.
Your example is not something that can be formally verified.
What I meant in my comment is that when you use formal verification to verify AI, it passes formal verification, but even if it passes that formal verification, the AI still can’t complete the task. The original article also talks about the importance of specifications in the AI era, but my point is that even if it passes formal verification, the AI still has problems. I’m not sure whether I misunderstood the original.
... somewhat disappointed the guy is now associated with AWS. I guess I was hoping for a non-profit organization.
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.
Nobody verifies it because there isn't a ZFS axiom system for software development and you first need a spec to prove anything-
Then perhaps fix Lean's type system, which isn't really understood and has holes.
Can these AI-monied people shut up for a single hour?