I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code. We (including agentic development) will move on from imperative languages, skipping functional and move to deterministic declarative languages.
Likely, a proliferation of experimental languages all somewhat akin to Typescript for SQL with significantly more nuanced operators to tersely capture the same outcomes as imperative languages.
They’ll compile down to be able to run performantly for game development or even for the Linux kernel (as if Linus would ever agree lol) but also they’ll be able to run on distributed execution engines with effectively a shared memory space, etc.
Allows for significantly more terse artifacts. Lower chance of hallucination, fewer output tokens, fewer thinking loop iterations and concise enough for humans to review (for domains that need it).
On top of that, additional theorem like syntax to drastically limit the ability of functions, etc. likely some sort of higher level effect system for verification. Used for many things like “constant time compilation for crypto functions”, and also “ensure acid compliance” for writes and reads in a local context, and things like “ensure only once delivery” for functions on a distributed execution engine.
At which point every program will be formally verified by default. You could think of it as AdaErlangSQL+++
Depends really. I tried some experiments towards a pretty uniform relational language for expressing ordinary logic, temporal logic, requirements etc. It does work, but there's some unexpected obstacles.
You'd think performance would be easy to achieve because you'd just write clear, high-level declarative facts and LLM + good optimiser + proof certification system will get you there in terms of performance. But you'll be surprised that relational/declarative specification gives you so much behaviour 'for free' that choosing what to actually compute from those relations is a very deliberate choice. It starts to look like finding an imperative-like path of demand through the relations. It seems that you get exactly the same problems but one level up.
Coming at it from another angle, we have historically made distributed systems manageable / 'verifiable' with RTOSs which give deterministic scheduling and locking primitives. We know that a task's max duration is its uninterrupted duration + max duration of all higher priority tasks which could pre-empt it, and so on. Deterministic pre-emptive scheduling and locking alone could be enough to prove a lot of invariants without full temporal logic, and writing code in 'RTOS logic' might be more natural for humans/LLMs than the more expressive and powerful alternatives.
What you're describing is a language that can effectively take a high-level design doc (limited to a formal language representing a pseudo-English-subset) and compile to almost arbitrarily complex, formally verifiable systems. I say systems because you're also implying these could essentially orchestrate distributed systems.
Which, if that were really possible, would be pretty good evidence of AGI. Or, at least, the end of 6-7 figure software engineer salaries. Conversely, I think it's a pipe dream. Writing a compiler that actually works well across such a broad range of hugely complex behaviors would itself be absurdly complex.
Also you would probably want to cache the compiler's output in git because running that compiler would take a long time, and you probably want the compiler's output to still be inspectable to human inspection. In the end that compiled artifact would look a lot like source code.
I think Rust's success in the AI space shows how useful formal proofs are, as Rust provides something very similar to that. Both because it helps with the understanding of LLMs, as well as with trusting the LLMs are not violating any basic properties (like please no nasal demons if the user sends a buffer larger than the allowed amount).
We've got inform7 with an English like language generating complex inform6 OOP optimized code since a few decades and the i7 compiler might even run under a Pentium II with 128MB of RAM under NetBSD. I6, under 32 and a Pentium. And maybe even less. ZMachine games themselves (the biggest v8 ones) under the Frotz interpreter, under a 486 and 8MB (with FreeDOS and Frotz). Or maybe an Amiga or a m68k Mac with the same amount of RAM.
Now imagine what AMD64 machine can do with 2GB of RAM (minimum baseline for legacy, maybe some C2D computer) today.
Check Inform7 for text adevntures. No AGI nor AI needed. On Inform6, it's a dumb simple OOP language where the structure it's almost self-evident. Classes, in-game objects with real-life attributes (enterable, a container for other objects, non-movable/pickable scenery and so on).
PD: inform7 can run on an RaspPi B+ or 25 year old PC's like nothing, and i6 down to 30 year old ones. The ZMachine adventures themselves, from any 16 bit computer and up.
I think it won't happen because people just care to much for performance. You already see this now. You see a ton of rewrites moving to rust even from higher level languages.
From the appendix [0]: "The proofs written by agents are just as 'good' as any other proof of the same theorem, in that they prove the equivalence theorem. However, it remains to be seen whether agents can scale this verbose proof style directly to more complex programs. Experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style, and scaling up requires the proofs to be structured around better modular abstractions and reasoning principles. If that is the case, how can we help agents discover and introduce the right abstractions to reduce this complexity? Does this require input from expert proof engineers, or can we extract common principles that can guide agents to discovering good abstractions that will enable scalable proofs?"
Some mathematicians have observed a similar pattern in the recent LLM proof drops, leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics. The sort of proofs done in formal verification are a pretty interesting litmus test for LLM reasoning since the systems considered aren't necessarily on distribution (compare with math where the "systems" and structures worked with, and proofs about them, make appearances in thousands of individual books) so the advantages in broad domain knowledge pretrained LLMs have over humans doesn't really buy you much. IMO this observation from Anthropic/Theorem lends more credibility to the convex hull hypothesis.
"leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics."
This was to be expected, llms are trained on a very large corpus of data, they 'look' like creative from our point of view, as humans don't have that much knowledge, so, if the LLM proposes something that a human does not know, it looks like creative. But they stay neural networks after all, so very good in interpolation, very bad at extrapolation.
Building new knowledge is extrapolation if it's truly outside the convex hull how the dataset.
I usually write code and ideas that are at the border of the convex hull, I haven't seen yet an llm being able to propose a really innovative solution. All the time they reuse building blocks that are already there. And I really tried pushing by making them creating proofs.
If I have an insight on some problem and I ask for the proof for it, it will usually be able to generate the proof, but that proof is never creative, and often it will use novel ideas only if I explain the novel idea. It will not come up with it alone. (And sometimes it's very hard to even explain the ideas, as it tends to return to knew waters)
Its only a data point, but I haven't seen a paper that handle this issue yet, and I don't expect them to magically become good at extrapolation due to the theory behind neural networks.
Writing proofs is just writing code in a niche language (that's what the Curry-Howard isomorphism is all about). Writing modular proofs with better abstractions is just writing modular code with better abstractions.
Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.
If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.
So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning
I agree with the observation but not the extrapolation. After all, RLing on sufficiently hard problems might cause agents to adopt better proof strategies emergently.
> LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics.
I love that “convex hull” analogy. LLMs can certainly serve as a channel for knowledge transfer. They can help spread knowledge and know-how throughout society, enabling breakthroughs that were simply held back by practical limitations (e.g. lack of money, time, or expertise). Personally, I think LLM is more valuable as a tool for democratizing knowledge than as artificial intelligence.
The difference between math and software verification: in math, the convex hull hypothesis implies that you don't go far beyond human capability, because the bottleneck is out of distribution generalization. In software verification, you can verify just about all the software that exists despite the convex hull hypothesis, because the bottleneck is just scale.
It’s exciting to see how low the barriers to fuzzing and formal proofs and higher verification standards like property based testing has become! It’s just a shame this LLMs are what it took, and even then adoption in the industry is slow.
For those skeptical, I've had decent success using formal verification for my Rust rewrite of Postgres. I wrote a compiler that can translate both Rust and C code into Lean. Once those two functions are in Lean, I have an LLM write a Lean proof that they behave identically.
So far, I've proven that about 12% of the code behaves the same when executed single-threaded. That works out to roughly 70k lines of C code. This has found very minor differences in behavior, such as how floating-point operations across platforms can produce different results.
I'm working on figuring out how to scale this up, but I don't see any fundamental limitation that would prevent this from scaling up further.
I've been using Opus 5.5 for pretty much everything
I tried giving Astra a shot. Since it scores better on math, I thought it might do better at writing Lean. I forgot the exact details, but that didn't end up being the case. I think it wasn't thinking holistically enough and tended to rabbit hole itself more
3. Inspection: checking what we built against the blueprint (the proofs)
This research makes the inspection close to perfect. But an inspection only checks the blueprint, not our vision, so a house built from the wrong blueprint can still pass a perfect inspection. The other half is making sure the blueprint matches our intent and stays that way while agents build. I'm working on that, so I think this is complementary:
> Claude can write a proof showing that a compiled program’s behavior satisfies the requirements of a formal spec (which is verified by an external proof checker). However, a proof checker can’t tell you whether your spec matches reality.
Been doing this at work for the past couple weeks. Extremely powerful to be able to have an agent open a PR with some experiments showing it makes some function faster using SIMD or CUDA, and just confidently merge it because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation.
I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.
Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.
All of human knowledge, experience, distilled down to idempotent instructions and code for specific tasks, functions, situations is fully testable against a near infinite amount of fuzz and attacks.
We do not question the strength of steel if properly treated.
Code is no different. We will enter the point where code is finally trusted as a carabiner and rope for the life of a climber.
This doesn't follow. We've had code as trusted as that for _decades_. Common criteria and EAL was certified at the end of the 20th century. Before that there was the rainbow series in the US dating back to the 1980s [1].
It's absolutely cool to see this sort of validation process get cheaper and easier, but it means nothing if no one cares enough to do it. EAL1 certification can be as cheap as a beefy server, but it's not commonly done because effectively no one cares.
As microsoft learned with the zune just because it's cheaper or better at the same price doesn't mean anyone will use it. Culturally, we have to make the effort of verifying code worth it.
Code needs to run on physical devices, which are prone to undervolting, bit flips, hardware bugs in specific batches, radiation, deterioration, and the like.
Preferably, I wouldn’t trust my life to a calculating device running on AA batteries while dangling from a rope.
We also have fully redundant systems. The elevator for example required Otis to do this fantastic demonstration 150 years ago and now we don't think twice about it.
Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.
> Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.
There's something called safety regulation. An installed elevator is very likely to have passed all the verification necessary for it to clear the safety bar. Same with the other devices you listed.
As for general code, it's mostly based on trust. But I see practices endorsed by the AI providers and trust is very low on my end.
The elusive 100%-coverage formal spec that covers every intended and unintended input, the interests of every stakeholder, and every possible user behavior? In the vibecoding era? No, the page has the decency to acknowledge this doesn't exist.
In the end, they settle on finding crashes with a conventional fuzzer, fixing crashes, and then... writing a formal proof that the crash is fixed? That seems... pretty pointless? Am I missing something here?
> Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.
However, you're correct that this is not formal verification in the sense of a correctness proof against a full specification validated to capture what the program is intended to do. Pretty impressive though.
What they did is tried to prove that the conventional fuzzer won't find crashes. Where they found counterexamples, they fixed the bug and tried again.
In essence, a fuzzer takes random samples out of a space of possible inputs that could crash. They proved that nothing in the space of possible inputs could crash.
This is a strictly more powerful result than a fuzzer could give you.
Yes. You are missing something. They are proving that for all possible inputs the program doesn't crash for a given size of potential inputs at the machine code level. The proof extends to an entire set of inputs and all the code it touches, not just the cases the fuzzer covers. In short, they have better coverage than any fuzzer.
Turning buggy software A into buggy software B, with all bells and whistles (and bugs included). This is useful for doing large-scale restructuring of codebases. You can verify you aren’t adding (or removing) bugs.
This seemed like a high possibility, but since our adoption of LLMs in software so far has mostly been to throw out best practices, I am skeptical that it will lead us to expanded verification.
It's like Bezos talking about how we're going to have 3 day work weeks while he makes his employees piss in a bottle.
Piss bottles are easily explained by rent though. You get more productive, so the landlord ups the rent, and you have to produce more for the people owning the scarce land (your landlord, the grocery store's landlord, the farmer, etc).
Software doesn't have this scarcity dynamic. People will use LLMs to build better sounder foundations (as rust is 'better' than c) and code quality will improve as we migrate to them. You won't get screwed on your rust++ license though to the point you have to piss in bottles.
It might be that I’m unfamiliar with the matter, but as I understand it, in order to prove a statement, the statement must correctly model the reality of the code.
In that case, how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?
Couldn’t it very well be that you proved something that wasn't actually your program?
If you have a model of the programming language, then you can make proofs about the source code itself. At this point, your assumption is that you are accuratly modelling the compiler.
You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.
> how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?
You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.
At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.
All this is going to do is move the problem up one layer. Sofware is fundamentally a representation of human expectations for the computer. How do you formally verify that?
Nohow, because the real world is informal. This is as far as coding can and will ever go, basically.
And like yes, it does just launder defects to a layer higher, but another way to phrase that in this case (and in many other cases) is that it raises the bar.
Instead of defects being mostly about nonsense minutia (relative to business logic), they are about actual design decisions and their correspondence to reality, i.e. the actual original goal and point of this god forsaken, navel-gazing field.
Strange to see Anthropic making this point. When I use Claude in my daily development and ticketing workflows, it doesn't seem to want to do formal verification of anything without me telling it to. It makes a lot of assumptions about the state of systems when it could very quickly write scripts to formally validate those states.
It's why unit tests are worthless when humans write them, and less than worthless when AI writes them. Same concept: you're testing yourself, of course you're going to pass with flying colors.
I took a different approach with this JavaCard VM I've been working on, first I had Claude implement the VM from the spec and then I had it implement a proof generator (also from the spec) so an identical bug would have to exist in both of them to make it through. Worked pretty well, the JCVM and bytecode verifier are both statically verified using ESBMC (which found a few bugs in that project so, win, win).
Now I have it working on a verifier for the bytecode transformations the optimizer uses, also using the static verification approach, to discover them all and ensure they are all valid. This one is seeming to be on track to making it fast enough to work on a real grammar as opposed to the 'academic grammars' the literature typically uses to prove the lemmas. Claude seems to be fighting this and has been working on the same refactor for over a week now so, we'll see...
I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code. We (including agentic development) will move on from imperative languages, skipping functional and move to deterministic declarative languages.
Likely, a proliferation of experimental languages all somewhat akin to Typescript for SQL with significantly more nuanced operators to tersely capture the same outcomes as imperative languages.
They’ll compile down to be able to run performantly for game development or even for the Linux kernel (as if Linus would ever agree lol) but also they’ll be able to run on distributed execution engines with effectively a shared memory space, etc.
Allows for significantly more terse artifacts. Lower chance of hallucination, fewer output tokens, fewer thinking loop iterations and concise enough for humans to review (for domains that need it).
On top of that, additional theorem like syntax to drastically limit the ability of functions, etc. likely some sort of higher level effect system for verification. Used for many things like “constant time compilation for crypto functions”, and also “ensure acid compliance” for writes and reads in a local context, and things like “ensure only once delivery” for functions on a distributed execution engine.
At which point every program will be formally verified by default. You could think of it as AdaErlangSQL+++
Depends really. I tried some experiments towards a pretty uniform relational language for expressing ordinary logic, temporal logic, requirements etc. It does work, but there's some unexpected obstacles.
You'd think performance would be easy to achieve because you'd just write clear, high-level declarative facts and LLM + good optimiser + proof certification system will get you there in terms of performance. But you'll be surprised that relational/declarative specification gives you so much behaviour 'for free' that choosing what to actually compute from those relations is a very deliberate choice. It starts to look like finding an imperative-like path of demand through the relations. It seems that you get exactly the same problems but one level up.
Coming at it from another angle, we have historically made distributed systems manageable / 'verifiable' with RTOSs which give deterministic scheduling and locking primitives. We know that a task's max duration is its uninterrupted duration + max duration of all higher priority tasks which could pre-empt it, and so on. Deterministic pre-emptive scheduling and locking alone could be enough to prove a lot of invariants without full temporal logic, and writing code in 'RTOS logic' might be more natural for humans/LLMs than the more expressive and powerful alternatives.
What you're describing is a language that can effectively take a high-level design doc (limited to a formal language representing a pseudo-English-subset) and compile to almost arbitrarily complex, formally verifiable systems. I say systems because you're also implying these could essentially orchestrate distributed systems.
Which, if that were really possible, would be pretty good evidence of AGI. Or, at least, the end of 6-7 figure software engineer salaries. Conversely, I think it's a pipe dream. Writing a compiler that actually works well across such a broad range of hugely complex behaviors would itself be absurdly complex.
Also you would probably want to cache the compiler's output in git because running that compiler would take a long time, and you probably want the compiler's output to still be inspectable to human inspection. In the end that compiled artifact would look a lot like source code.
I think Rust's success in the AI space shows how useful formal proofs are, as Rust provides something very similar to that. Both because it helps with the understanding of LLMs, as well as with trusting the LLMs are not violating any basic properties (like please no nasal demons if the user sends a buffer larger than the allowed amount).
We've got inform7 with an English like language generating complex inform6 OOP optimized code since a few decades and the i7 compiler might even run under a Pentium II with 128MB of RAM under NetBSD. I6, under 32 and a Pentium. And maybe even less. ZMachine games themselves (the biggest v8 ones) under the Frotz interpreter, under a 486 and 8MB (with FreeDOS and Frotz). Or maybe an Amiga or a m68k Mac with the same amount of RAM.
Now imagine what AMD64 machine can do with 2GB of RAM (minimum baseline for legacy, maybe some C2D computer) today.
Check Inform7 for text adevntures. No AGI nor AI needed. On Inform6, it's a dumb simple OOP language where the structure it's almost self-evident. Classes, in-game objects with real-life attributes (enterable, a container for other objects, non-movable/pickable scenery and so on).
PD: inform7 can run on an RaspPi B+ or 25 year old PC's like nothing, and i6 down to 30 year old ones. The ZMachine adventures themselves, from any 16 bit computer and up.
I think it won't happen because people just care to much for performance. You already see this now. You see a ton of rewrites moving to rust even from higher level languages.
So Inform7 like languages generating Rust code and then binary code and linked against the OS.
From the appendix [0]: "The proofs written by agents are just as 'good' as any other proof of the same theorem, in that they prove the equivalence theorem. However, it remains to be seen whether agents can scale this verbose proof style directly to more complex programs. Experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style, and scaling up requires the proofs to be structured around better modular abstractions and reasoning principles. If that is the case, how can we help agents discover and introduce the right abstractions to reduce this complexity? Does this require input from expert proof engineers, or can we extract common principles that can guide agents to discovering good abstractions that will enable scalable proofs?"
Some mathematicians have observed a similar pattern in the recent LLM proof drops, leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics. The sort of proofs done in formal verification are a pretty interesting litmus test for LLM reasoning since the systems considered aren't necessarily on distribution (compare with math where the "systems" and structures worked with, and proofs about them, make appearances in thousands of individual books) so the advantages in broad domain knowledge pretrained LLMs have over humans doesn't really buy you much. IMO this observation from Anthropic/Theorem lends more credibility to the convex hull hypothesis.
[0] https://www-cdn.anthropic.com/files/4zrzovbb/website/6867ead...
"leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics."
This was to be expected, llms are trained on a very large corpus of data, they 'look' like creative from our point of view, as humans don't have that much knowledge, so, if the LLM proposes something that a human does not know, it looks like creative. But they stay neural networks after all, so very good in interpolation, very bad at extrapolation. Building new knowledge is extrapolation if it's truly outside the convex hull how the dataset.
I usually write code and ideas that are at the border of the convex hull, I haven't seen yet an llm being able to propose a really innovative solution. All the time they reuse building blocks that are already there. And I really tried pushing by making them creating proofs.
If I have an insight on some problem and I ask for the proof for it, it will usually be able to generate the proof, but that proof is never creative, and often it will use novel ideas only if I explain the novel idea. It will not come up with it alone. (And sometimes it's very hard to even explain the ideas, as it tends to return to knew waters)
Its only a data point, but I haven't seen a paper that handle this issue yet, and I don't expect them to magically become good at extrapolation due to the theory behind neural networks.
Writing proofs is just writing code in a niche language (that's what the Curry-Howard isomorphism is all about). Writing modular proofs with better abstractions is just writing modular code with better abstractions.
Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.
If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.
So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning
[0] https://creusot.rs/
[1] https://flux-rs.github.io/
[2] https://lean-lang.org/use-cases/aeneas/
I agree with the observation but not the extrapolation. After all, RLing on sufficiently hard problems might cause agents to adopt better proof strategies emergently.
> LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics.
I love that “convex hull” analogy. LLMs can certainly serve as a channel for knowledge transfer. They can help spread knowledge and know-how throughout society, enabling breakthroughs that were simply held back by practical limitations (e.g. lack of money, time, or expertise). Personally, I think LLM is more valuable as a tool for democratizing knowledge than as artificial intelligence.
Sounds like a software problem.
The difference between math and software verification: in math, the convex hull hypothesis implies that you don't go far beyond human capability, because the bottleneck is out of distribution generalization. In software verification, you can verify just about all the software that exists despite the convex hull hypothesis, because the bottleneck is just scale.
https://knowyourmeme.com/memes/they-feed-us-poison /jk
It’s exciting to see how low the barriers to fuzzing and formal proofs and higher verification standards like property based testing has become! It’s just a shame this LLMs are what it took, and even then adoption in the industry is slow.
For those skeptical, I've had decent success using formal verification for my Rust rewrite of Postgres. I wrote a compiler that can translate both Rust and C code into Lean. Once those two functions are in Lean, I have an LLM write a Lean proof that they behave identically.
So far, I've proven that about 12% of the code behaves the same when executed single-threaded. That works out to roughly 70k lines of C code. This has found very minor differences in behavior, such as how floating-point operations across platforms can produce different results.
I'm working on figuring out how to scale this up, but I don't see any fundamental limitation that would prevent this from scaling up further.
Which models do you see to be productive for the task of writing lean? Big fan of pgrust.
I've been using Opus 5.5 for pretty much everything
I tried giving Astra a shot. Since it scores better on math, I thought it might do better at writing Lean. I forgot the exact details, but that didn't end up being the case. I think it wasn't thinking holistically enough and tended to rabbit hole itself more
Building a house has three layers:
1. Vision: what we want (our intent)
2. Blueprint: the spec we wrote (our design)
3. Inspection: checking what we built against the blueprint (the proofs)
This research makes the inspection close to perfect. But an inspection only checks the blueprint, not our vision, so a house built from the wrong blueprint can still pass a perfect inspection. The other half is making sure the blueprint matches our intent and stays that way while agents build. I'm working on that, so I think this is complementary:
https://github.com/pullboard-dev/pullboard
> Claude can write a proof showing that a compiled program’s behavior satisfies the requirements of a formal spec (which is verified by an external proof checker). However, a proof checker can’t tell you whether your spec matches reality.
Imagine having a formal spec for reality!
Been doing this at work for the past couple weeks. Extremely powerful to be able to have an agent open a PR with some experiments showing it makes some function faster using SIMD or CUDA, and just confidently merge it because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation.
How do you gain confidence that your theorem actually applies to your code?
My Rocq setup directly reads my actual code. And I fuzz my semantic models against the real machine.
I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.
Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.
Does this require having a Rocq semantics of LLVM IR? Which one do you use?
This flows.
All of human knowledge, experience, distilled down to idempotent instructions and code for specific tasks, functions, situations is fully testable against a near infinite amount of fuzz and attacks.
We do not question the strength of steel if properly treated.
Code is no different. We will enter the point where code is finally trusted as a carabiner and rope for the life of a climber.
This doesn't follow. We've had code as trusted as that for _decades_. Common criteria and EAL was certified at the end of the 20th century. Before that there was the rainbow series in the US dating back to the 1980s [1].
It's absolutely cool to see this sort of validation process get cheaper and easier, but it means nothing if no one cares enough to do it. EAL1 certification can be as cheap as a beefy server, but it's not commonly done because effectively no one cares.
As microsoft learned with the zune just because it's cheaper or better at the same price doesn't mean anyone will use it. Culturally, we have to make the effort of verifying code worth it.
[1]: https://en.wikipedia.org/wiki/Rainbow_Series
Code needs to run on physical devices, which are prone to undervolting, bit flips, hardware bugs in specific batches, radiation, deterioration, and the like.
Preferably, I wouldn’t trust my life to a calculating device running on AA batteries while dangling from a rope.
Pace makers, dialysis machines, brake lines.
We also have fully redundant systems. The elevator for example required Otis to do this fantastic demonstration 150 years ago and now we don't think twice about it.
Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.
> Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.
There's something called safety regulation. An installed elevator is very likely to have passed all the verification necessary for it to clear the safety bar. Same with the other devices you listed.
As for general code, it's mostly based on trust. But I see practices endorsed by the AI providers and trust is very low on my end.
Formal verification against what?
The elusive 100%-coverage formal spec that covers every intended and unintended input, the interests of every stakeholder, and every possible user behavior? In the vibecoding era? No, the page has the decency to acknowledge this doesn't exist.
In the end, they settle on finding crashes with a conventional fuzzer, fixing crashes, and then... writing a formal proof that the crash is fixed? That seems... pretty pointless? Am I missing something here?
From the article:
> Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.
However, you're correct that this is not formal verification in the sense of a correctness proof against a full specification validated to capture what the program is intended to do. Pretty impressive though.
That's not what they did.
What they did is tried to prove that the conventional fuzzer won't find crashes. Where they found counterexamples, they fixed the bug and tried again.
In essence, a fuzzer takes random samples out of a space of possible inputs that could crash. They proved that nothing in the space of possible inputs could crash.
This is a strictly more powerful result than a fuzzer could give you.
Yes. You are missing something. They are proving that for all possible inputs the program doesn't crash for a given size of potential inputs at the machine code level. The proof extends to an entire set of inputs and all the code it touches, not just the cases the fuzzer covers. In short, they have better coverage than any fuzzer.
Turning buggy software A into buggy software B, with all bells and whistles (and bugs included). This is useful for doing large-scale restructuring of codebases. You can verify you aren’t adding (or removing) bugs.
This seemed like a high possibility, but since our adoption of LLMs in software so far has mostly been to throw out best practices, I am skeptical that it will lead us to expanded verification.
It's like Bezos talking about how we're going to have 3 day work weeks while he makes his employees piss in a bottle.
Piss bottles are easily explained by rent though. You get more productive, so the landlord ups the rent, and you have to produce more for the people owning the scarce land (your landlord, the grocery store's landlord, the farmer, etc).
Software doesn't have this scarcity dynamic. People will use LLMs to build better sounder foundations (as rust is 'better' than c) and code quality will improve as we migrate to them. You won't get screwed on your rust++ license though to the point you have to piss in bottles.
It might be that I’m unfamiliar with the matter, but as I understand it, in order to prove a statement, the statement must correctly model the reality of the code. In that case, how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?
Couldn’t it very well be that you proved something that wasn't actually your program?
If you have a model of the programming language, then you can make proofs about the source code itself. At this point, your assumption is that you are accuratly modelling the compiler.
You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.
> Couldn’t it very well be that you proved something that wasn't actually your program?
Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.
> how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?
You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.
At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.
TLA mentioned, previous related discussions about the topic:
"What TLA+ can and can't check" https://news.ycombinator.com/item?id=49909056
"The internet discovers TLA+. Now what?" https://news.ycombinator.com/item?id=49863600
What a tiny subset of all TLA+ articles (a very popular topic on HN)...
2017: Leslie Lamport: Video course on TLA+ (328 points, 74 comments) https://news.ycombinator.com/item?id=13918648 (219 points, 2018, 17 comments) https://news.ycombinator.com/item?id=16956778
2017: Writing correct lock-free and distributed stateful systems in Rust, with TLA+ (374 points, 94 comments) https://news.ycombinator.com/item?id=14373359
2019: TLA+ model checking made symbolic (197 points, 51 comments) https://news.ycombinator.com/item?id=21662484
2019: Introduction to TLA+ Model Checking in the Command Line (176 points, 44 comments) https://news.ycombinator.com/item?id=18937214
2019: Learn TLA+ (387 points, 92 comments) https://news.ycombinator.com/item?id=19661329 (310 points, 2020, 58 comments) https://news.ycombinator.com/item?id=22393653 (254 points, 2022, 64 comments) https://news.ycombinator.com/item?id=33010645 (350 points, 2022, 75 comments) https://news.ycombinator.com/item?id=31952643
2020: Using TLA+ in the Real World to Understand a Glibc Bug (166 points, 76 comments) https://news.ycombinator.com/item?id=24958504
2026: Hunting a 16-year-old SQLite WAL bug with TLA+ (239 points, 29 comments) https://news.ycombinator.com/item?id=48730953
...
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
Yeah... usages of TLA+ within the realm of LLM is kinda newish, wouldn't you agree?
One wonders how deep is Anthropic's queue of marketorials.
All this is going to do is move the problem up one layer. Sofware is fundamentally a representation of human expectations for the computer. How do you formally verify that?
Nohow, because the real world is informal. This is as far as coding can and will ever go, basically.
And like yes, it does just launder defects to a layer higher, but another way to phrase that in this case (and in many other cases) is that it raises the bar.
Instead of defects being mostly about nonsense minutia (relative to business logic), they are about actual design decisions and their correspondence to reality, i.e. the actual original goal and point of this god forsaken, navel-gazing field.
I'm curious if increased adoption of formal verifications would increase migration of legacy COBOL to modern systems.
I found that even with LLMs making sure the formal specification covers what you actually want is challenging.
How do you actually know what the LLM proved is what you want?
Did they remember what OpenAI did with Lean and Math Proofs?
OpenAI wrote some lean that pass the validate, write a math paper that feel plausible, but the paper don't match what's in lean.
Anthropic is now translating programs into Rocq proof. The same can happen.
Don't get me wrong -- this process can help catch some bug. but this is far from a proof
Strange to see Anthropic making this point. When I use Claude in my daily development and ticketing workflows, it doesn't seem to want to do formal verification of anything without me telling it to. It makes a lot of assumptions about the state of systems when it could very quickly write scripts to formally validate those states.
It's why unit tests are worthless when humans write them, and less than worthless when AI writes them. Same concept: you're testing yourself, of course you're going to pass with flying colors.
I would disagree that this is not “formal verification” as that discounts the entire software supply chain and how attacks actually show up.
Is this end to end verification? Cause this sounds closer to validation than verification.
I took a different approach with this JavaCard VM I've been working on, first I had Claude implement the VM from the spec and then I had it implement a proof generator (also from the spec) so an identical bug would have to exist in both of them to make it through. Worked pretty well, the JCVM and bytecode verifier are both statically verified using ESBMC (which found a few bugs in that project so, win, win).
Now I have it working on a verifier for the bytecode transformations the optimizer uses, also using the static verification approach, to discover them all and ensure they are all valid. This one is seeming to be on track to making it fast enough to work on a real grammar as opposed to the 'academic grammars' the literature typically uses to prove the lemmas. Claude seems to be fighting this and has been working on the same refactor for over a week now so, we'll see...