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
d0mine 11 hours ago [-]
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).
rramadass 13 hours ago [-]
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?
chamomeal 16 hours ago [-]
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
Ericson2314 16 hours ago [-]
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.
chamomeal 14 hours ago [-]
> 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
gls2ro 14 hours ago [-]
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.
kccqzy 16 hours ago [-]
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.
praveenrajus 13 hours ago [-]
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
fkozlowski 11 hours ago [-]
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.
te_chris 16 hours ago [-]
Yeah, LLMs make setting up the annoying things like PBT and mutation testing easy. It’s great.
PandaRider 18 hours ago [-]
> ... 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)
johnbender 17 hours ago [-]
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.
This is a vibecoded project, not a resource for learning modeling for formal verification.
beecasthurlbow 12 hours ago [-]
If you use agents to generate formal verification, how do you tell if the properties that are verified are the correct ones?
AlienMuse 2 hours ago [-]
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.
turtleyacht 12 hours ago [-]
Applications: implications, simulations, and experiments. Gobble the frontier; wring out the usable.
mkesper 8 hours ago [-]
This reads as gibberish.
qbit42 8 hours ago [-]
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
voidhorse 7 hours ago [-]
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.
Ohentis 6 hours ago [-]
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).
fspeech 14 hours ago [-]
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.
charlieyu1 7 hours ago [-]
I just don’t know why we are using a verification that is hard to read and write for humans
robswc 7 hours ago [-]
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.
westurner 14 hours ago [-]
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.
dist-epoch 20 hours ago [-]
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"
jdw64 19 hours ago [-]
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.
rramadass 10 hours ago [-]
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 ;-)
skydhash 2 hours ago [-]
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.
jdw64 3 hours ago [-]
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.
moi2388 18 hours ago [-]
Can you try to get it to only specify interfaces first? Then tests, the write code to implement
jdw64 20 hours ago [-]
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.
Leynos 16 hours ago [-]
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.
jdw64 14 hours ago [-]
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.
yksalun 18 hours ago [-]
[flagged]
Phemist 19 hours ago [-]
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.
baq 18 hours ago [-]
I see not only me tried to give astra insufficiently described tasks
jdw64 18 hours ago [-]
It seems you've summarized my problem properly. Haha.
Gabriel54 18 hours ago [-]
Your example is not something that can be formally verified.
jdw64 18 hours ago [-]
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.
zhengzefeng 18 hours ago [-]
[flagged]
shevy-java 16 hours ago [-]
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.
Rendered at 05:56:49 GMT+0000 (Coordinated Universal Time) with Vercel.
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
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?
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
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.
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.
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.
Does anyone have resources on learning modelling for formal verification? (Does not have to be in Lean)
https://lamport.azurewebsites.net/tla/book.html https://logicforprogrammers.com/ https://softwarefoundations.cis.upenn.edu/
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.
mostly jk, although agents themselves are of course getting better at detecting whether a formal spec is faithful to a natural language spec
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.
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.
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
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)
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 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"
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.
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 ;-)
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.
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 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.
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.
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.