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
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).
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
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.
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
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.
I think there's some bad nomenclature here. "Property based testing" literally means you're writing properties, which can be verified formally, or randomly (fuzzing / constrained random testing).
For example in SystemVerilog you can write properties (literally with the `property` keyword), and then they can be checked in simulation, and with formal tools.
TLA+ can do the same I believe - there are tools to verify a model randomly or formally.
> ... 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.
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.
In my view, AI currently relies primarily on human-developed tools for verification. Although AI has used some reinforcement learning (RL) algorithms to identify the paths humans have taken at each level, these paths are essentially still based on human mathematical tools and require confirmation by human experts. We need a more revolutionary framework to provide AI for mathematics with new methods and verification pathways.
You don't. You place unwavering faith in the machine god.
This is why, for formal methods to really be the next step, we'll need deterministic source to CoC language compilers, and we'll need to go back again.
Lean is kind of an unfortunate, cargo cult choice because it only compiles to C. Really for software we should use a prover that has a lot more targets, like Danfy. Even Rocq (formerly Coq) can compile down to several functional languages, which is more than we can say for lean.
As usual, the AI crowd latched on to the first solution that came to mind, and thanks to its prominence in mathematics applications recently just lazily are starting to try and apply it to computing, without actually understanding anything or weighing trade offs. Of course, now we are basically stuck with Lean since the models will have been trained hard on it. At least it's a CoC language, but now we need to build a bunch of extra compilation around it for this to really work.
Most of this feels fairly orthogonal to the question asked. And the reasons lean are chosen are fairly simple: it is designed to also be used for programming and it's actually successful. Compiling to C is fairly obviously a bad choice (well I guess not obviously, people keep implementing languages this way for some reason) but arguably one of the least important factors in choosing which prover to use. The alternatives to lean would be Idris (which is both unsound and unpopular), ats (which is unpopular) or rocq (which is more reasonable but still is mostly an academic project).
Compiling to C seems obviously an excellent choice for compiling a language to. It is a good choice as a target language, and one can rely on a lot of existing tooling, a stable standard, good interoperability, and wide platform support. It is also simply enough to be modeled precisely.
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 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?
> 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.
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.
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 ;-)
The whole things kinda read as an idealistic and very wrong view of software engineering.
If you take a look at "real" code out there and it's evolution, you'll find that the main thing that drives it is the set of requirements. On the other side you have the platform (standard and 3rd party libraries as well as frameworks). Add to that is the set of algorithmic techniques (including design patterns).
By analyzing the requirements, you will discern that often they're composed of sub-problems that are generic (which is where you algorithms techniques comes in). And some are already solved (libraries). Often there's a common shape to the requirements (or some of them) that can be extracted into "frameworks".
So what's left then is the assembly. But often requirements are evolving concepts. So you don't want your structure (architecture) to be that rigid. You can't really know the direction of evolution, so you try to predict it in some way and add flexibility in a few places. This is more an art, but there are general techniques that works well enough.
The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces. A program is always part of an information system. Means data come in, got processed, and go out. And here is the majority of development type is consumed, ensuring that the data is correctly processed.
Programming concepts like type checking, memory safety, paradigms (oop, functional, relational,...), formal verification,... are all about data. Code always come in second place. So think hard about your data and its transformation.
> The whole things kinda read as an idealistic and very wrong view of software engineering.
You have not correctly understood what i wrote.
The above is a battle-tested methodology based on experience/studies/trial-and-error and now being adapted to AI with extra tweaks. Labour which was the main bottleneck earlier is now cheap and hence we can afford to be "idealistic" since the tool is immensely powerful.
You need to expand and iterate each stage above (both individually and as a group with previous stages) in stepwise-refinement to get to what you want.
The rest of your comment is just generic platitudes and some common red herrings which i often see on HN, viz.
> main thing that drives it is the set of requirements...By analyzing the requirements,..But often requirements are evolving concepts.
Everybody just keeps parroting this without understanding. Requirements change but always in a staged manner and not willy-nilly. Hence there is always a window of time when your "Requirements Document" is frozen and you can implement a PoC/Prototype against it. The is the "naive" MVP i mention above. Later when requirements change you reiterate and regenerate your prototype and continue.
These are all covered under (1.c) above where you explicitly list out what to use and what not to use. These are all part of the "architectural constraints".
> So what's left then is the assembly...So you don't want your structure (architecture) to be that rigid. You can't really know the direction of evolution, so you try to predict it in some way and add flexibility in a few places. This is more an art, but there are general techniques that works well enough.
This is covered under (1) above where i enforce rigid adherence to "modularity" and "separation of concerns" by making each module's public interface narrow and extensible (eg. ioctl like) and its parameters future-proof by using versioned struct/class inheritance (eg. sockaddr). These are all well-known code patterns used in OS implementations/libraries.
> The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces.
This is taken care of by having modules follow the LKM model with ioctl interface as explained above.
> Programming concepts like type checking, memory safety, paradigms (oop, functional, relational,...), formal verification,... are all about data. Code always come in second place. So think hard about your data and its transformation.
DbC methodology is the quintessential "data-driven" programming since the pre/post/inv are predicates to establish sets of data values on which the subsequent code can operate safely i.e. DbC establishes the data path for the code.
> Labour which was the main bottleneck earlier is now cheap and hence we can afford to be "idealistic" since the tool is immensely powerful.
This labour was not the main bottleneck. I’m ready to bet that coding is a small part of the daily activities of a dev.
> Later when requirements change you reiterate and regenerate your prototype and continue.
That is incredibly wasteful. Requirements are set agains a world model that always evolves against its own set of constraints. Which does ties into the flexibility argument. No need to reinvent the wheel, when only a few things varies and some just stay true for years and decades..
>> The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces
> This is taken care of by having modules follow the LKM model with ioctl interface as explained above.
Nope, it’s not. This is related to having a good mental model of how your software process data, not related to how you design your interface.
—-
As I said, your comments put “code” as a first place citizen, which no experience dev does. What I argue about is that it’s always about data, the rules that it follow, which will then be realized by code.
> DbC methodology is the quintessential "data-driven" programming since the pre/post/inv are predicates to establish sets of data values on which the subsequent code can operate safely
Like the one above. You don’t write code and assert which type of data that it can handle. That’s a fool errand as the outside world is naturally messy. You define the data first, and then write the code. Meaning when the data changes, the code needs to evolve. You need to have a very good mental how that changes propagate, which you won’t have of you just regenerating code.
That’s why no one builds a factory to produce factories. Although there are common elements, a factory is designed for the product it will create. So you start from the product, you don’t start from the factory. Your methodology is a framework for building factories, but with no mention of any product.
Thank you so much for the advice. I’m a beginner in this area, so your help has been a great help to me. When I did it myself, verification kept being satisfied, but it stayed in a state with no progress; but after working based on your comment, progress seems to have sped up.
Since I’m a freelance programmer, my workflow is far removed from other people’s (there’s no review, and I mostly deliver programs based on whether they run), and I had no place to hear advice from seniors. But rramadass always helps me. Thanks to the advice you gave me, I was able to study formal verification and also study ADTs, and explore a broader world.
Some local regressions still exist, but the big looping around has decreased compared to before. It still seems long-running agents can’t fully replace humans yet.
I’m always grateful, and thank you for not getting annoyed and for giving me advice even though I’m always lacking. Have a good day.
Thank you so much.
May I save your comment and write it on my homepage later?
Your advice seems like it will be a big help. Since I’m mostly doing things by reading manuals and books and running into problems myself, certain problems get solved quickly, but there are sections where I get stuck like this, and I always get a lot of help from you. Thank you always.
The stages in the above methodology should be expanded, which as i suggested, you can have AI do it for you. Note that you must be the "human-in-the-loop" and give the explicit go ahead after every stage i.e. checkpoint.
As part of your "Architectural Constraints", always list your specific libraries/frameworks/design patterns/code techniques that you are familiar with and want to be used while excluding everything else. For example you could say something like; "Do not use any design patterns outside of the GoF book", "Use <name> async framework only" etc. Guardrails are everything with AI.
The idea is that you should be able to read the generated code without too much difficulty.
Note that we are using DbC as one level of Formal Verification at runtime during development only. For verifying it statically we can have it mapped onto Lean4 (using tools) or to a SMT solver via SMT-LIB; see my comment here - https://news.ycombinator.com/item?id=50108112
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?
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.
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.
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.
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.
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
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.
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
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.
I think there's some bad nomenclature here. "Property based testing" literally means you're writing properties, which can be verified formally, or randomly (fuzzing / constrained random testing).
For example in SystemVerilog you can write properties (literally with the `property` keyword), and then they can be checked in simulation, and with formal tools.
TLA+ can do the same I believe - there are tools to verify a model randomly or formally.
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?
In my view, AI currently relies primarily on human-developed tools for verification. Although AI has used some reinforcement learning (RL) algorithms to identify the paths humans have taken at each level, these paths are essentially still based on human mathematical tools and require confirmation by human experts. We need a more revolutionary framework to provide AI for mathematics with new methods and verification pathways.
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
You don't. You place unwavering faith in the machine god.
This is why, for formal methods to really be the next step, we'll need deterministic source to CoC language compilers, and we'll need to go back again.
Lean is kind of an unfortunate, cargo cult choice because it only compiles to C. Really for software we should use a prover that has a lot more targets, like Danfy. Even Rocq (formerly Coq) can compile down to several functional languages, which is more than we can say for lean.
As usual, the AI crowd latched on to the first solution that came to mind, and thanks to its prominence in mathematics applications recently just lazily are starting to try and apply it to computing, without actually understanding anything or weighing trade offs. Of course, now we are basically stuck with Lean since the models will have been trained hard on it. At least it's a CoC language, but now we need to build a bunch of extra compilation around it for this to really work.
Most of this feels fairly orthogonal to the question asked. And the reasons lean are chosen are fairly simple: it is designed to also be used for programming and it's actually successful. Compiling to C is fairly obviously a bad choice (well I guess not obviously, people keep implementing languages this way for some reason) but arguably one of the least important factors in choosing which prover to use. The alternatives to lean would be Idris (which is both unsound and unpopular), ats (which is unpopular) or rocq (which is more reasonable but still is mostly an academic project).
Compiling to C seems obviously an excellent choice for compiling a language to. It is a good choice as a target language, and one can rely on a lot of existing tooling, a stable standard, good interoperability, and wide platform support. It is also simply enough to be modeled precisely.
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.
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
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)
... somewhat disappointed the guy is now associated with AWS. I guess I was hoping for a non-profit organization.
He is also the chief architect and cofounder of the Lean FRO, the associated non-profit: https://lean-lang.org/fro/team/
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.
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 ;-)
The whole things kinda read as an idealistic and very wrong view of software engineering.
If you take a look at "real" code out there and it's evolution, you'll find that the main thing that drives it is the set of requirements. On the other side you have the platform (standard and 3rd party libraries as well as frameworks). Add to that is the set of algorithmic techniques (including design patterns).
By analyzing the requirements, you will discern that often they're composed of sub-problems that are generic (which is where you algorithms techniques comes in). And some are already solved (libraries). Often there's a common shape to the requirements (or some of them) that can be extracted into "frameworks".
So what's left then is the assembly. But often requirements are evolving concepts. So you don't want your structure (architecture) to be that rigid. You can't really know the direction of evolution, so you try to predict it in some way and add flexibility in a few places. This is more an art, but there are general techniques that works well enough.
The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces. A program is always part of an information system. Means data come in, got processed, and go out. And here is the majority of development type is consumed, ensuring that the data is correctly processed.
Programming concepts like type checking, memory safety, paradigms (oop, functional, relational,...), formal verification,... are all about data. Code always come in second place. So think hard about your data and its transformation.
> The whole things kinda read as an idealistic and very wrong view of software engineering.
You have not correctly understood what i wrote.
The above is a battle-tested methodology based on experience/studies/trial-and-error and now being adapted to AI with extra tweaks. Labour which was the main bottleneck earlier is now cheap and hence we can afford to be "idealistic" since the tool is immensely powerful.
You need to expand and iterate each stage above (both individually and as a group with previous stages) in stepwise-refinement to get to what you want.
The rest of your comment is just generic platitudes and some common red herrings which i often see on HN, viz.
> main thing that drives it is the set of requirements...By analyzing the requirements,..But often requirements are evolving concepts.
Everybody just keeps parroting this without understanding. Requirements change but always in a staged manner and not willy-nilly. Hence there is always a window of time when your "Requirements Document" is frozen and you can implement a PoC/Prototype against it. The is the "naive" MVP i mention above. Later when requirements change you reiterate and regenerate your prototype and continue.
Note that the gp already had his UML design and only wanted a way to convert it to code. Hence i did not discuss requirements gathering and analysis here. Nonetheless, i had discussed this earlier in some previous comments - https://news.ycombinator.com/item?id=48274873 https://news.ycombinator.com/item?id=48264680
> Platform...libraries...frameworks...design patterns...
These are all covered under (1.c) above where you explicitly list out what to use and what not to use. These are all part of the "architectural constraints".
> So what's left then is the assembly...So you don't want your structure (architecture) to be that rigid. You can't really know the direction of evolution, so you try to predict it in some way and add flexibility in a few places. This is more an art, but there are general techniques that works well enough.
This is covered under (1) above where i enforce rigid adherence to "modularity" and "separation of concerns" by making each module's public interface narrow and extensible (eg. ioctl like) and its parameters future-proof by using versioned struct/class inheritance (eg. sockaddr). These are all well-known code patterns used in OS implementations/libraries.
> The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces.
This is taken care of by having modules follow the LKM model with ioctl interface as explained above.
> Programming concepts like type checking, memory safety, paradigms (oop, functional, relational,...), formal verification,... are all about data. Code always come in second place. So think hard about your data and its transformation.
DbC methodology is the quintessential "data-driven" programming since the pre/post/inv are predicates to establish sets of data values on which the subsequent code can operate safely i.e. DbC establishes the data path for the code.
> Labour which was the main bottleneck earlier is now cheap and hence we can afford to be "idealistic" since the tool is immensely powerful.
This labour was not the main bottleneck. I’m ready to bet that coding is a small part of the daily activities of a dev.
> Later when requirements change you reiterate and regenerate your prototype and continue.
That is incredibly wasteful. Requirements are set agains a world model that always evolves against its own set of constraints. Which does ties into the flexibility argument. No need to reinvent the wheel, when only a few things varies and some just stay true for years and decades..
>> The assembly itself is a matter of data and process. How each module is initialized, its lifecycle, which data it consumes, which data it produces
> This is taken care of by having modules follow the LKM model with ioctl interface as explained above.
Nope, it’s not. This is related to having a good mental model of how your software process data, not related to how you design your interface.
—-
As I said, your comments put “code” as a first place citizen, which no experience dev does. What I argue about is that it’s always about data, the rules that it follow, which will then be realized by code.
> DbC methodology is the quintessential "data-driven" programming since the pre/post/inv are predicates to establish sets of data values on which the subsequent code can operate safely
Like the one above. You don’t write code and assert which type of data that it can handle. That’s a fool errand as the outside world is naturally messy. You define the data first, and then write the code. Meaning when the data changes, the code needs to evolve. You need to have a very good mental how that changes propagate, which you won’t have of you just regenerating code.
That’s why no one builds a factory to produce factories. Although there are common elements, a factory is designed for the product it will create. So you start from the product, you don’t start from the factory. Your methodology is a framework for building factories, but with no mention of any product.
Thank you so much for the advice. I’m a beginner in this area, so your help has been a great help to me. When I did it myself, verification kept being satisfied, but it stayed in a state with no progress; but after working based on your comment, progress seems to have sped up.
Since I’m a freelance programmer, my workflow is far removed from other people’s (there’s no review, and I mostly deliver programs based on whether they run), and I had no place to hear advice from seniors. But rramadass always helps me. Thanks to the advice you gave me, I was able to study formal verification and also study ADTs, and explore a broader world.
Some local regressions still exist, but the big looping around has decreased compared to before. It still seems long-running agents can’t fully replace humans yet. I’m always grateful, and thank you for not getting annoyed and for giving me advice even though I’m always lacking. Have a good day. Thank you so much.
May I save your comment and write it on my homepage later? Your advice seems like it will be a big help. Since I’m mostly doing things by reading manuals and books and running into problems myself, certain problems get solved quickly, but there are sections where I get stuck like this, and I always get a lot of help from you. Thank you always.
Sure, go ahead and use my comment for your homepage, share it, extend it etc. See also my other comment with some more explanations - https://news.ycombinator.com/item?id=50326359
The stages in the above methodology should be expanded, which as i suggested, you can have AI do it for you. Note that you must be the "human-in-the-loop" and give the explicit go ahead after every stage i.e. checkpoint.
As part of your "Architectural Constraints", always list your specific libraries/frameworks/design patterns/code techniques that you are familiar with and want to be used while excluding everything else. For example you could say something like; "Do not use any design patterns outside of the GoF book", "Use <name> async framework only" etc. Guardrails are everything with AI.
The idea is that you should be able to read the generated code without too much difficulty.
Note that we are using DbC as one level of Formal Verification at runtime during development only. For verifying it statically we can have it mapped onto Lean4 (using tools) or to a SMT solver via SMT-LIB; see my comment here - https://news.ycombinator.com/item?id=50108112
See also; Combining Tests and Proofs with Contracts for Better Software Verification by Bertrand Meyer et al. - https://dl.acm.org/doi/10.1145/3793869
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.
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.
Carl Sagan has! The man was pre-scient.
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.
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.