Specifications: Were hopefully correctly modeled to the Problem.
In IEEE terms:
> Verification: "Are we building the product right?"
> Validation: "Are we building the right product?")
You can write mathematically flawless code that highly efficiently solves the wrong problem.
---
While I think formal verification is the future (essential for cybersecurity), it's not a silver bullet for the other 2 items, which are way more ambiguous. I think however they can all iterate on each other and improve the project overall, but it still depends on competent steering
If you have had experiences with good approaches for verification Validation & Specification framework, do let us know about them.
> A good moment to remind everyone: Verification: Code does what it says. Validation: Code does what Specifications say.
Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."
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.
Every verification needs a spec, and in this case the spec is the Postgres implementation. I think we can and should do a lot better than taking 2.6 million lines of C code as the spec.
In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.
A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].
> I wrote a compiler that can translate both Rust and C code into Lean
How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts
I haven't yet. My main goal has been to find as many bugs as possible. While bugs could still slip through because my compiler is incorrect, I'm still finding a good number, so I think it's worth it.
Does your bilingual [Rust|C] -> Lean compiler fork rustc or clang, or other? 12% is promisingly high. I'm still hoping for a world where you can prove critical behavior w static analysis cheaply and practically. The overlap of LLMs and PLT feel under-explored to me
I tried several approaches to support both C and Rust. I tried using LLVM bytecode, but that ended up being way too low-level. The proofs ended up being gargantuan.
I also tried converting CBMC's intermediate representation, "GOTO Programs" to Lean. This seemed worth a shot because CMBC supports C and Kani adds support for Rust. Unfortunately, Kani's Rust-to-GOTO conversion caused a massive blow-up in code size.
What I ended up doing was converting both GOTO Programs and MIR (Rust's IR) to my own custom IR. The IR is low-level enough to convert both languages, but high-level enough to keep the code relatively concise. I then run simplification passes over the IR and compile it to Lean.
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
Opus 5.5 is a god tier model, but for serious large scale work, nothing beats getting at least three non-similar models to repeatedly refine a super detailed plan before any code is written.
Right now my consortium is Opus 5.5, Grok 4.7 and Muse Wonder. These three are different enough that their insights are very complementary. Once a plan is detailed enough, any decent model can execute on it successfully, but I personally like Grok’s ability to stick to the plan. (And no 5-hour quota!)
Always fascinating to see Grok marketing in the wild. Always the same pattern of mentioning it innocently at the beginning of the message, then doubling down with a specific praise at the end. Well it's rare enough that it could also be a set of users who organically made it their mission to get HN to care about Grok.
idk - I had good experiences with Grok. At least before Gemini 3.7 flash came out it was one of the best fast and cheap models. Back with Fable 5.0, I was having issues with fuzz testing because I kept hitting the security safeguards. Grok ended up being the best model at the time I could get to do what I wanted
Proving the code works single threaded is a stepping stone to eventually proving the code works under concurrency. It may be surprising, but very little of the Postgres code deals with concurrency. For the most part they've isolated the parts that deal with concurrency to a small number of subsystems. At least by volume of code, the vast majority of it is single threaded
Im 35, Im screwed if they get their way. I'm not going to go to the trades, I quit construction when I was 27 because of how much I loved programming. I wanted to kill myself basically everyday working in the construction industry. I drank my twenties away because of how much it sucked. Ive been sober for years now entirely because of programming and actually loving what I do. But this company is stealing that from me, in many different ways.
I invested a ton of my life and my entire life savings into this transition. Now Im being screamed at everyday to go be an electrician because Anthropic claims they're going to solve the halting problem in some round about way, they dont even have to do what they claim. They just have to convince 20% of industry that they will, and guys like me will never get a chance to work long enough to retire.
I really don't think they'll suceeed, but if they do, Im going to be homeless coding from the public library because im not starting over again.
A lot of people think more jobs overall will be created from this. I sort of agree. However, our day to day has changed so much. The problems that I found fulfilling to solve are now handed off to LLMs, but at the same time I can build the things I want to build easier and faster. There are tradeoffs for sure. I'm trying to stay positive though.
> A lot of people think more jobs overall will be created from this.
Be sure to distinguish between "jobs" and "good jobs" (that are enough to survive and even prosper on). Jobs that pay pittances can be created til the cows come home.
Yeah, there are conflicting views in the industry about whether LLM's will make more jobs overall or kill off jobs. The ostentatiously virtuous thing is the ability for developers to make software faster.
I've built some tools that genuinely help me manage my life tasks that improve my quality of life irl, but a lot of stuff I've built has been built to allow me to build more things like itself faster... And I ask myself, for what? Haha
yeah like I've used AI to build me app to automate editing short clips which would have taken me a long time to make, if I coded them by myself. This is good but then it make you question why a software firm would hire you or keep you if there is a tool that can do this.
I feel ya. I've been grappling with the fact how this field has been completely uprooted.
On one hand, I see this as another layer of abstraction: I don't know assembly, yet I can command the processor to do stuff via python. LLMs can be seen as another layer of abstraction that allows us to write higher volumes of even more complex software.
On the other hand, I can see how programmers can go the route of the chimney sweepers. I try to be optimistic but feel fearful as well.
Hang in there! What you can build knowing how to code is drastically different from what promptards can build. Imagine trying to build a car without knowing anything about car building - you’d just get the most generic boring clunker anyone can design.
My first question was “How do they know the proof correctly corresponds to the software they are checking?”
They say “ While this is an enormous volume of proof code, virtually none of it needs to be manually reviewed. The Rocq proof checker ensures that the spec is correctly satisfied by the proof. As a result, the only artifacts that a developer needs to trust are:
The formal models of RISC-V and of Linux processes;
The exact theorem statements that were proved;
The Rocq proof checker itself.”
What are the formal models of
RISCV and Linux? I’m guessing they allow translation of RISCV code directly into Rocq proofs?
I’d love to see more info about their workflow of code -> proof. Or even an open source tool
Exactly. How do they now that the spec that was generated was correct? Is the spec also AI generated, and could the models lie to make a spec they can verify, just like they lie to make tests pass?
It is also interesting how the LLM optimists are leaning on tools like Rocq and Lean to save them from the mess of uncertainty and confusion. These are tools created by people who understood their code and worked with deeply with type theory etc. People can keep thinking they can get away with making products from vibes, but down in the infrastructure they still have to depend on people thinking and building carefully.
It is hypocritical to campaign for "nobody will look at code anymore" while depending on the hard work of people who carefully look at code.
I've noticed that people (including myself) are becoming too lazy with LLMs.
Trying to become even lazier by skipping code reviews and then vibe-coding formal software verification will get you into trouble.
In my experience with software verification, perfect is the enemy of good. My recommendation is to start with a software design you actually understand, and then try to understand how to map your requirements to something you can prove.
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+++
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.
AGI will accelerate it, but way before agentic development I learned this was the future when I worked at Amazon. I no longer have access to the internal talks about it (amazing to watch) but here is a public link worth reading:
You don't really need compilers anymore. LLM's can write programs over any AST and provide an equivalence proof provided you have good semantics for the source and target.
Semantics of a language describe the behaviour of a sentence in that language when executed. When you have semantics in a theorem prover you can construct equivalence proofs between programs expressed in different languages (or proofs that a compiler from one language to another is semantics preserving).
I was mostly referring to accuracy when I said "good" above, in the sense that they should reflect the actual behaviour of the language they describe.
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).
```
SELECT A, B, Sum(C)
FROM Somewhere
GROUP BY ALL
```
Very few developers look at the underlying “source code” that this SQL compiles into. Very few people even read the “source code” that tsc outputs.
The reality is the lowest level checkpoint worth looking at and understanding is the highest possible abstraction layer which preserves 100% of the needed precision and flexibility that the product being built requires.
Also, you’d just use something like sscache or just .o files to speed up compilation. It’d be unusual to store compiler MIR/LIR in git.
I think the important part will be figuring out what we need from the higher level language that achieves 100% of the precision and flexibility of Rust for the product being built.
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.
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.
I've enjoyed embedding declarative syntax inside imperative languages, like LINQ and prolog as a dsl. The imperative code can express temporality much easier, and the declarative code allows you to throw that away when you don't want it.
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.
I think this is indeed the direction, but am wondering is anyone actually trying it right now? Love to explore it.
I think for now the answer to adaerlangsql+++ is just Rust - but its semantics have always been about human usability.
Humans have this thing where we can only keep 7 things at once and have to juggle our context, but recall seems much more broad than model contexts.
If we were to start designing a language and toolkit based around LLM context sizes, limitations and quirks - how would that look?
Also terseness and operators are one thing, but what if it’s the other way around - English words etc - can have a much bigger vocabulary of things that can be done but can easily be generated on the fly.
For a new LLM language realistically you would need to probably either write or convert a shit ton of software to it first if you are to train an adequate model on top of it …
And also what about “IDEs” for agents? So far they are clumsily using human tools - just looking Claude string along bash loops and greps to try to eek out meaning form code _it itself had written a week ago_ is frankly frustrating.
There must be a better way and some rich agent specific tooling for code exploration and verification.
Anthropic stance has always been “yeah we tested them all, grep is better” but I still am not convinced - just by the fact that it constantly fails one or two attempts before “figuring it out” yeah it’s fast anyway but it could be _faster_ and could allow the agent to “think” in code space more and not have to validate itself at every minute step …
What I want tho would be Rust+Akka for example. There has to be a distributed execution mechanism that is as seamless as Java’s GC. Then the distributed execution mechanism needs to evolve to also be as light weight and “zero cost” while being seamless like Rust’s compile time memory management.
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.
I’m generally cautious/sceptical about the current LLM hype, but if that did ever happen and it worked to a useful degree, it might truly be a significant advance. I’m not saying that just because of the LLMs themselves, though.
To reach that point, we would first need to overcome the classic problems in this area:
1. How can you specify the required behaviour for a system in precise detail without ending up with a specification language that is essentially another programming language with similar complexity to the ones we use today?
2. How do you solve the sufficiently smart compiler problem so that producing reasonably efficient and reliable implementations of those declarative specifications is not only viable but expected?
And then, if you still need someone (let’s call them a “developer”) to carefully specify the required behaviour of the system in detail, and you also know how to reliably generate a good implementation of a specification, how much value is left for LLMs to add in this picture?
Maybe LLMs really could be trained to reliably produce good implementations in that scenario? Never say never, but it seems more likely to me that we would develop deterministic algorithms for doing so. That’s already a very hard problem that a lot of smart people have explored, but if a solution could be found, most likely it would be strictly better than relying on LLMs in this part of the process.
Maybe there would still be a role for LLMs to convert natural language problem statements into specifications? Maybe for systems that don’t really matter, that would be enough and a big time saver. However, I’m sceptical about how much time it would be likely to save for systems that did need to work, where you would still need careful design and review of all the detailed specifications by developers anyway.
Maybe LLMs would end up in a similar role to the scaffolding tools that are popular in some ecosystems today, where you feed in some basic choices and the tool then produces a first pass at the files and code you might need, which you take as a starting point for the real work but without wasting so much time on boilerplate? That seems realistic and useful, but it’s a relatively small part of what would then be the overall development process.
In short, I would love for the existence of LLMs/agents to push us towards those better programming languages and tool chains, but if that did ever happen, I wonder how much benefit LLMs/agents could still offer once developers had the more powerful languages and tools available and could work at a “higher level of abstraction” themselves.
These are the good good questions. I wish I was smart enough to answer them.
I think the best bet is to let a hundred developers play at it for a bit. There will be a lot of bespoke domain specific declarative languages. They will over time learn from each other to be better and better.
Experiments like GoogleSql’s pipe syntax https://docs.cloud.google.com/bigtable/docs/reference/sql/pi... getting pushed even further and further. That’s where I’d put my money. Cloudflare might be another candidate for building such a programming language for the distributed compute and memory “machine”.
(Also once we are there)
I think there will be even better questions: What does programming CRDTs like a blockchain that reconcile across Mars and Earth look like? and in that way, LLMs will constantly be useful helpers to explore the state/latent space.
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.
i dont even think that it would be possible to build a declarative language that is flexible enough to do what an imperative language is capable of without being an imperative language itself
> 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.
Linus doesn't have to care, MirageOS already exists for OCaml, and I'm pretty sure there's something like MirageOS for Rust...
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.
Automated proofs do sound very neat but I think they'll be constrained to a vanishingly small set of already paranoid domains like cryptography, aerospace, etc. Everywhere else is going to spend the dividends on shipping more unvetted code faster, we're just trading discipline for velocity.
Llm adoption has just accelerated people's tendencies. Slop generators generate more slop. They're also finding and fixing bugs that have existed for decades. The societal incentives towards slop we will have to figure out but that's not new - for folks not on that wavelength and for when we get over that impulse at some point it's good if it can also do this. Just in general so sure does write a hell of a lot of tests. If it gets good at it this could pretty easily just become part of the agent loop and we get whatever wins we can from that.
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.
Time is finite. People’s problems that can be solved by software is also finite. There’s diminishing returns in improving software. Rewriting bash in rust, and then testing the result would barely help anyone. Also the real world (where inputs come from) is messy. You can have the perfect mechanism (memory safety), but that grain of sand (corrupted or unexpected data) can still make it behave erratically (wrong result).
AI is the dark energy of engineering - it pushes us further apart, faster. Some of us get pushed towards slop, others towards formal spec validation, and as time goes it will be harder and harder to see each other.
A while back a knowledgeable man was a philosopher, and they could all easily talk to each other and understand. As time went we split up - we have philosophy doctors in various fields who have very little to talk about.
This happened again when the term “engineer” fractured (even before software engineering). Software engineering itself fractured, too.
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.
At least in arts, there is a true "creative" element complicated to replicate at least in the current LLMs. True artistic invention involves a "spirit of rule-breaking" that pushes culture forward. If AI is only being trained on past data, it then struggles to make the non-linear, revolutionary creative jumps we've seen throughout history.
For instance, the transition of music from the 1950s to the Beatles, then to Nirvana, hip-hop, and beyond. Before Beatles, there wasn't such thing as Beatles. Before Nirvana, there wasn't anything that sounded like that. Of course you can point out underground bands doing something like that around that era, but stray way back in time to like 1940s and chances of hearing something like Nirvana are near zero.
True art is not easy to make. It is, rather, difficult. If you lower the difficulty to make art, then it is not already a piece of art. It is just another product down the line of plenty of copy cats. Art involves risk taking that AIs I don't think are capable of producing. Art is a medium to express human emotions, and the inherent concept here is that it will end up being consumed by another human being, and it has value because you know that another human being was on the other side of the table making it. Even if you do something you consider art for yourself with an AI, the human being on the other side was, well... you. You prompted it and you guided it. I don't believe people in general would be contempt with an endless stream of autonomous AI generated stuff (if they invent such loop) because it would not only be generic, repetitive and predictable at some point, but also the fact that you know its AI it destroys the whole vibe. Same as if you get an email and you don't know if it was an AI or human behind it. If it was a human being, great, you feel a connection there. If it was AI, well... that sucks to no end, and I guess that is for a very good reason.
Although I'm using art here as the argument for creativity, I believe there may be something analogous to scientific leaps and discoveries. To my understanding, people who seem to be fairly successful in uncover the truths of the universe via science also happen to be pretty good when it comes to some artistic endeavors, even if its only about consuming and appreciating art and not necessarily creating it. So, there might be some link in creativity there. I'm open to be wrong, of course. Creativity is about risk taking and pushing the edges, not re-iterating upon what's been already there.
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
Curry-Howard doesn't buy you any shortcuts to capability. Surely no expense has been spared in training models to write good (well modularized, robust, generic etc.) code, and yet they still write slop (poorly structured, overfit to specification gaps, etc.) We see the same sloppish habits in their mathematics, perhaps transported along the CH iso. So "train[ing] agents to write better proofs" seems to me like a grand challenge problem for AI research, just like getting them to write good code. It won't be solved just by noticing that the two problems are isomorphic: we'll keep getting models that are a little better at grinding out proofs, hence a little better at grinding out programs, but the abstraction wall won't magically drop in either world just because the same limited behaviors can be transported along CH.
The key is to make general intelligence, and train models in regimes that generalize well among many domains, rather than just a bunch of math proof tricks that don't generalize.
I think LLMs have demonstrated tons of generalization already, but I concede that being good at theorem provers don't automatically translate into being good at other forms of programming and vice versa. But the labs should probably focus on generalizing rather than optimizing for each subfield of programming individually.
Also as an aside, I meant that the use of theorem provers for proving theorems is just programming, that is, Lean, Rocq etc. are programming languages. They are functional programming languages and they invoke Curry-Howard as a reason for them to work, like, at all. And that's why their reasoning is essentially intuitionistic
You make a compelling argument, but, empirically, when you optimize code for performance, you end up with an unreadable mess that breaks all abstractions; but every time I've substantially optimized a proof for performance [of proof checking], I've ended up with better abstractions and more modularity.
That's super interesting. I wonder if you've tried optimizing for type-checking duration of a richly dependently typed program and gotten viscerally nicer code out of that.
> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.
> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.
- - -
This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.
If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.
One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people
Nobody (sane) does that.
Lots of people have the implementer write the tests. But this only seems like a bad thing because of an unfortunate terminology collision:
- Microsoft culture: tests are adversarial verification.
- Google culture: tests are executable documentation.
Both of these things are important. It's really unfortunate we call both of them "tests".
At Microsoft, (verification) tests are written by a different engineer than the one who wrote the code under test. VLSI/Hardware works like this too.
At Google, (documentation) tests are written by the person who wrote the code, because it's their job to document it, and because the point of documentation-tests is to make sure other people who modify your code don't break it.
> 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.
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.
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.
This is not just plausible but in fact the most likely result.
We already have plenty of evidence of this phenomenon in programming. LLMs are awesome for working on human-written or at least human-reviewed codebases.
But when you set them loose without a human around to force them to refactor their code into something that fits in meatbag-brain-sized contexts, they drift into the ghastly nightmare of the Anthropocene (go ahead, take a look at the leaked source code for Claude Code). They can handle this for a while, especially if you're doubling your model's weight count every four months.
But when you stop doing that, they choke on their own spaghetti.
It's like Feynman said about teaching -- great theoretical physicists need to re-explain the basics to students from time to time in order to force them to come up with not just the correct physical laws, but the simplest version of those laws. Take away that constraint -- IAS or LLM -- and eventually it all goes wrong.
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.
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.
In essence this lets you verify any property you want for a given function, as long as it can be expressed as a fuzz test. Specifically, you can express your property with an assert, and then prove that it never fires. This is nice because it keeps everything in one language, rather than having to translate the whole program into Rocq and then express your desired property as a Rocq theorem.
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.
The main thing they focused on in that is just cybersecurity. Formal verification to try and get rid of surface area for vulnerabilities. Seems like a good idea idk. It also sounds like they're just kinda getting started with it - we'll have to see what opus 5.6 or 5.7 looks like after they've RLed on it a bunch
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.
No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other.
Ah, interesting. I went with Ghidra p-code which seems ok but what I didn't really appreciate going in was how much of the platform API surface you have to describe before you can prove pretty much anything at all.
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:
Along these lines, we used Codex to collaboratively build an alloy model for verifying the authorization model of GoodMem. After building the model, we implemented the code based on it, and, while there could be a gap in the translation process, several hours of red-teaming the server (w/attacker source code access) to try and produce a privilege escalation attack using GLM 5.3 failed.
Alloy is a tool I tried to learn many years ago, but I never learned it well enough to use it for formal verification of a complex production system. Credit goes to agentic coding tools for making it a reality.
If you use LLMs to digest and summarise software maybe it can help to improve formalisation. In contrast if you use LLMs to produce more code this is contra-dictionary. More codes increases the bug surface circa logarithmically and correspondingly makes formalisation much harder as well. I want to see LLMs be used to strip away code. Only then will I believe they’re really actually good at what they’re doing.
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.
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.
I think it's a really illustrative example of how to play to AI's strengths. No human would dream of writing 600,000 lines of Rocq to verify one binary. The whole approach is so insane that it probably wouldn't even occur to them. But Claude has no concept of tedium, and will happily fill out lemmas all day long until the job is done. To me that's what's significant about this result: it's not about scaling up an existing technique, it's about using scale itself as the basis of a new technique.
I have a skill for using Verus with Rust [1]. I think they found a nice way to integrate proofs with the language. The verify skill I use lists proofs as a possible technique [2] and the project instructions have instructions on using it, but only a very small fraction of the code base I am using this on has proofs. Anyone can now have an LLM write proofs but its still difficult to know when they are more productive than other techniques and to relay that advice to an LLM.
How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.
I was going through an experiment trying to spec out a simple caching system in Lean. I was getting Gemini to help me run through doing this, step by step. At one point it writes out this statement with a proof to show something, the specifics of which I forget, but it was some simple property of the cache. I stare at it for a while thinking to myself this can't be right, it was some sort of plain tautological statement that didn't really say anything, like saying 1 = 1.
I give it to Opus 5.5 and it basically confirmed my gut feeling that it was useless.
I'd like to rely more on formal verification. I like the idea of starting out with specs in a formal setting and designing software that way. The problem is it's hard to do right, and my point is even with AI, it's hard to do right.
That's the nice thing about the approach described in the blog: you use the same Rocq theorem for every binary (it just says "this binary doesn't crash") and then you express the property you want in your language of choice. For example, to prove that your compression algorithm round-trips, you would write something like assert(x == decompress(compress(x))).
I fully agree it’s harder to read. I do chip design and I feel like formal is more common in this area, but I generally restrict it to very simple properties that are easy to understand without having to mentally solve a sudoku puzzle.
It’s to easy to write an assertion that looks like it checks what you want it to, and gives you a false confidence when it passes, only to figure out after a field failure that it wasn’t checking what you thought at all.
But I’d pay for a commercial set of properties and assertions that had guarantees, and not worry about their complexity. For something standard like cache protocols and bus protocols.
Other cases it needs to be pretty straightforward to grasp by a peer reviewer in minutes, or it’s not worth it.
But when you can hit the sweet spot, a set of easily understood properties (or complex but trusted properties), formal can save massive amounts of time.
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.
I mean ... The thing about formal verification is that you can write the extremely slow but correct version of your code and then have an optimizer write a much more efficient version with a proof of correctness.
For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.
If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.
> 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.
> 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.
> Specifically, Claude proved that these programs will always exit normally without triggering memory-safety errors or failing assertions, for every input less than 64 MB and ...
I don't get what you mean? Granted, I didn't even try reading your message, since the language that you're using, English, is not sound, complete, decidable (or even defined).
About time, too. I studied formal software and hardware verification “before AI” and automated reasoning and cognitive architectures were just in need of scale. People are struggling with the inherent meaningmaking of taking formalism seriously in the world. It’s easy to roll your eyes (and I do a lot of that myself) but I have a lot of sympathy. It took many years of dedicated focus for me to convince myself the validity of automated reasoning / externalized cognition.
I designed Sharpee and generated the code with Claude Code. About six months in I had Claude generate a manual for the language. Then I had this crazy idea of testing the manual with a completely dummy instance of Claude in a VM.
Nothing solidified Sharpee more than “compiling” this manual chapter by chapter.
But even that left gaps. I then designed a true DSL called Chord that compiles to Sharpee and this really ramped up the solidity of Sharpee.
Except COBOL systems are often easier to formally verify than modern systems.
They're often simpler, and whole classes of security vulnerabilities are mitigated by design. My favorite example is SQL injection mitigated by having proper access controls in the DB. Why prove about every SQL statement that it cannot be nefarious, when we can just prove it about the connecting user? The user access carries the intent of what the application program wants to do with the database, in a separate channel, independently of the complexity of the application.
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...
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 wouldn’t call them worthless. I guess it depends on the unit. But also having someone or something independently write tests is generally better than testing your own code.
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.
You do it by comparing to something that is “known” to be good.
I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.
Proving two things are equivalent is a major component of formal.
For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.
A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.
Talk is cheap, show me the code. Claude generated a formally verified Python interpreter in Rust? Bullshit. Anthropic would have published it if they did, like that dogshit C compiler publicity stunt. That they won't even show it indicates that this is so misleading as to be a lie. They generously give themselves the grace of describing it as a "subset" of Python interpreter, and I believe them -- I can formally verify a "subset" of Python quite easily, but nobody will be impressed when they look at what that really means. Why was it tested with "1.7 million randomly generated" Python programs and not any real-world Python programs that already exist? Because the subset doesn't cover what anybody would consider to actually be Python.
Hmm? I had Claude Opus 4.6 implement a .NET compiled language that is Python-like (we already have IronPython, I wanted something Python-like that treated .NET as its entire runtime) language in about two (maybe three sessions tops?) of 1M token context windows, and the first two times I only used roughly 400 to 600k tokens? When Anthropic dropped the 1M context window update, I put it to the test.
Anyway, my custom (currently paused because I'm taking on a much more ambitious compiler project with Claude... just to push the limits) language can build ASP .NET applications, and a bunch other things. I also took the Rust approach to types, all method signatures must have types defined, type hints are inferred when declaring new values from the value on the right.
I've also had Claude rewrite legacy C# projects with 100k+ lines of code, fully in Rust, long before Opus 5.0. I've spent the last year pushing the limits with Claude, including reimplementing existing software, which people are catching on to now, and I've managed to get rather far in some cases.
So I wouldn't be surprised if yes, Claude can implement Python, mind you, there's Python interpreter coded in Python in what was it? 500 lines of Python? You can build a Python stack machine bytecode interpreter in like 60 ~ 80 lines of Python code.
Would not surprise me if you can trim a C programming language interpreter down in terms of lines of code when you rewrite it in Rust especially when you have access to a much more functional language, not to mention Rust took the best bits out of OCaml it could to make itself very efficient at writing compilers / languages (so they could write their own compiler in Rust...).
I am also having Claude building me a much smaller compiler, which started out in under 500 lines of Python, but as I got more ambitious it had to write more code for my language, it was meant to be a slightly less restrictive Go, the Python basically converts the syntax to C which then compiles anywhere. Havent put that one on GitHub since I'm still tinkering with it.
I notice you haven't touched that repo once since the month you prompted for it. I don't doubt that you generated some cute little prototype that compiles something. I do doubt that it's something actually suitable for anybody to use for programming. My own experiments with having frontier models attempt to implement my own language have all been dire. Even with a rigorous specification and a set of hand-written programs showing both the input of my language and the asm it should output, it managed to create something that compiles exactly those programs and completely fails in real-world use beyond that. So too with Claude's own C compiler experiment; even with C's unbelievably rigorous test suites that give it a deterministic guideline and actionable feedback every time it fucks up, it was still shit. If they merely gave it a C specification, without the decades of human-written tests, there is a snowball's chance in hell it would produce anything worth using.
I think you answered your own problem: telling it what assembly you're expecting, get it to build the foundation before you start asking it how the tiles should look.
Right now I'm working on a compiler / runtime for a more complicated language than Python or C and while its "slower" I know that once it's done through this run I'll be able to have it focus on optimizations, especially with rigorous tests that some languages have to test their compilers. I have plans to run back to Culebral, but I have to scratch a bigger itch I've had, people like you who've told me repeatedly that an LLM cannot be used to build a compiler. So here I am, slowly chugging at it, getting decades of developer effort worked through every week.
If I'm wrong, so be it, if I'm right, it'll be fun to release. :)
It doesn't take a decade to write a compiler for a language. If you're putting months of your own effort into it, it's not clear that the LLM is even increasing your productivity.
I think these developments should be done with care and cognizance of the user. I worry that formalism may have trouble scaling and interacting with user intent. LLMs will (and already do in my experience) construct a formalism for your application that may be provable to some archetype -- but separate from reality and separate from your conception. The Claude user experience of rulings is already at a cultural limit among users -- the excitement over the linguistic 'improvements' of the Opus 5.5 release are a case in point. Formalism is only one axis here and usability is another. This could be a problematic development if done lopsidedly.
Is formal verification the path forward? Meh... I dont think so. Does it have applications in some areas: yes. But this is just more robust "unit testing".
Anthropic keeps trying to convince you that "one agent" will do the job. It does so with the statement "We built 36 small verification tasks from real OSS-Fuzz code. Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. We expect this trend to continue as models are trained on long verification tasks."
But this is not the path forward. Robust E2E, durable (can your app go from python to rust with out loosing tests) Simulation/Emulation tests are the way. This is an "in bulk" and "brute force" activity. Go look at TigerBeetle for an example of this in practice. Go look at how oxide is doing testing.
Can a swarm of cheaper agents write these tests more effectively that Anthropics premium products. I assure you that it can.
If you look at OAI's actions (hugging face hack) and anthropic own publication on its version control AI is not a best of breed solution its a brute force hammer at it till you get what you need solution.
> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.
I wish people would learn a little computer science before making this kind of impossible claim. And I wonder how many people read claims like this and accept them without investigation.
The Turing Halting Problem (THP) invalidates the above claim, on all nontrivial software systems, forever.
The THP (1937) is derived from Gödel's Incompleteness Theorems (1931), and the latter are not a matter of opinion.
For those with limited attention spans, ask yourself this: How does the foolproof program checker check itself?
The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.
Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
I think incompleteness theorem means that you can't guarantee the agents will always be able to converge on a proof, since you can't have both completeness and soundness (and we obviously need soundness since that's the whole point of a theorem prover).
But most real-world programs are maybe not that "expressive" since we don't even want them to be capable of infinite loops (since those would often be denial of service vectors). So you should usually be able to prove that they halt (and presumably other properties as well), especially when you allow agents to rewrite things to pull out invariants that make proofs easier (as they did).
And for cases where getting clean invariants are difficult, I imagine you can just hack it by having some cutoff which trivially ensures things always halt. (Not sure what the equivalent would be for "no bug" proofs, probably rejecting things that are technically valid input per spec but seem unusual?)
While I completely agree with 3uru, where it can get stuck is if your system contains a pseudorandom generator or some other cryptographic shenanigans. These are programs deliberately made difficult to analyze and reason about.
I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).
That's a good point, although couldn't you usually black-box those and assume the invariants we expect of those primitives are in fact true? E.g. you don't need to bother trying to prove properties about your prng itself, you can just prove how your program behaves under a random oracle model.
> The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.
No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.
> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.
That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".
> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.
The language is Turing-complete, not the program. Rice's theorem says that we can't have a program that verifies a non-trivial property for all other programs. It doesn't say we can't verify that property for some programs. That would imply you could never know anything about a program.
A good moment to remind everyone:
Verification: Code does what it says.
Validation: Code does what Specifications say.
Specifications: Were hopefully correctly modeled to the Problem.
In IEEE terms:
> Verification: "Are we building the product right?" > Validation: "Are we building the right product?")
You can write mathematically flawless code that highly efficiently solves the wrong problem.
---
While I think formal verification is the future (essential for cybersecurity), it's not a silver bullet for the other 2 items, which are way more ambiguous. I think however they can all iterate on each other and improve the project overall, but it still depends on competent steering
If you have had experiences with good approaches for verification Validation & Specification framework, do let us know about them.
> A good moment to remind everyone: Verification: Code does what it says. Validation: Code does what Specifications say.
Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."
[1] https://en.wikipedia.org/wiki/Formal_verification
It's still great if the assertions in your code are provably correct.
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.
Every verification needs a spec, and in this case the spec is the Postgres implementation. I think we can and should do a lot better than taking 2.6 million lines of C code as the spec.
In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.
A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].
[1]: https://prela-lang.org/
[2]: https://github.com/remysucre/prela/tree/sqlstorm
[3]: https://github.com/remysucre/prela/tree/doom/
> In general, the spec must be human readable, and I believe to achieve that we must do away with SQL
Eh. Carthago delenda est? Why?
> I wrote a compiler that can translate both Rust and C code into Lean
How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts
> How do you verify this compiler is correct?
I haven't yet. My main goal has been to find as many bugs as possible. While bugs could still slip through because my compiler is incorrect, I'm still finding a good number, so I think it's worth it.
Did you consider using an established Rust verification toolchain like Aeneas?
Edit: I don't do this often, but why is my question being downvoted? Is this question not allowed?
AFAICT, Aeneas only supports a safe subset of Rust. I needed something that could support all of Rust
Have you heard of Aeneas? In case you did, what are your opinions on it? Specifically, why you didn't choose it for your project.
From what I can tell Aeneas only supports safe Rust. I need something that works with both C and unsafe Rust.
Does your bilingual [Rust|C] -> Lean compiler fork rustc or clang, or other? 12% is promisingly high. I'm still hoping for a world where you can prove critical behavior w static analysis cheaply and practically. The overlap of LLMs and PLT feel under-explored to me
pgrust is incredible btw
Thanks!
I tried several approaches to support both C and Rust. I tried using LLVM bytecode, but that ended up being way too low-level. The proofs ended up being gargantuan.
I also tried converting CBMC's intermediate representation, "GOTO Programs" to Lean. This seemed worth a shot because CMBC supports C and Kani adds support for Rust. Unfortunately, Kani's Rust-to-GOTO conversion caused a massive blow-up in code size.
What I ended up doing was converting both GOTO Programs and MIR (Rust's IR) to my own custom IR. The IR is low-level enough to convert both languages, but high-level enough to keep the code relatively concise. I then run simplification passes over the IR and compile it to Lean.
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
Opus 5.5 is a god tier model, but for serious large scale work, nothing beats getting at least three non-similar models to repeatedly refine a super detailed plan before any code is written.
Right now my consortium is Opus 5.5, Grok 4.7 and Muse Wonder. These three are different enough that their insights are very complementary. Once a plan is detailed enough, any decent model can execute on it successfully, but I personally like Grok’s ability to stick to the plan. (And no 5-hour quota!)
Always fascinating to see Grok marketing in the wild. Always the same pattern of mentioning it innocently at the beginning of the message, then doubling down with a specific praise at the end. Well it's rare enough that it could also be a set of users who organically made it their mission to get HN to care about Grok.
idk - I had good experiences with Grok. At least before Gemini 3.7 flash came out it was one of the best fast and cheap models. Back with Fable 5.0, I was having issues with fuzz testing because I kept hitting the security safeguards. Grok ended up being the best model at the time I could get to do what I wanted
Same experience on my vibe coding side project. Astra seems autistic to the context, Claude seems more of an open minded partner with good taste.
So far, I've proven that about 12% of the code behaves the same when executed single-threaded.
Dude, this is a database.
Concurrency is the source of all the hard stuff in databases.
Databases without concurrency are super-trivial.
I don't see any fundamental limitation that would prevent this from scaling up further.
The fact that you've dodged all the hard stuff is a pretty fundamental limitation.
Proving the code works single threaded is a stepping stone to eventually proving the code works under concurrency. It may be surprising, but very little of the Postgres code deals with concurrency. For the most part they've isolated the parts that deal with concurrency to a small number of subsystems. At least by volume of code, the vast majority of it is single threaded
Im 35, Im screwed if they get their way. I'm not going to go to the trades, I quit construction when I was 27 because of how much I loved programming. I wanted to kill myself basically everyday working in the construction industry. I drank my twenties away because of how much it sucked. Ive been sober for years now entirely because of programming and actually loving what I do. But this company is stealing that from me, in many different ways.
I invested a ton of my life and my entire life savings into this transition. Now Im being screamed at everyday to go be an electrician because Anthropic claims they're going to solve the halting problem in some round about way, they dont even have to do what they claim. They just have to convince 20% of industry that they will, and guys like me will never get a chance to work long enough to retire.
I really don't think they'll suceeed, but if they do, Im going to be homeless coding from the public library because im not starting over again.
A lot of people think more jobs overall will be created from this. I sort of agree. However, our day to day has changed so much. The problems that I found fulfilling to solve are now handed off to LLMs, but at the same time I can build the things I want to build easier and faster. There are tradeoffs for sure. I'm trying to stay positive though.
> A lot of people think more jobs overall will be created from this.
Be sure to distinguish between "jobs" and "good jobs" (that are enough to survive and even prosper on). Jobs that pay pittances can be created til the cows come home.
Yeah, there are conflicting views in the industry about whether LLM's will make more jobs overall or kill off jobs. The ostentatiously virtuous thing is the ability for developers to make software faster.
I've built some tools that genuinely help me manage my life tasks that improve my quality of life irl, but a lot of stuff I've built has been built to allow me to build more things like itself faster... And I ask myself, for what? Haha
yeah like I've used AI to build me app to automate editing short clips which would have taken me a long time to make, if I coded them by myself. This is good but then it make you question why a software firm would hire you or keep you if there is a tool that can do this.
I feel ya. I've been grappling with the fact how this field has been completely uprooted. On one hand, I see this as another layer of abstraction: I don't know assembly, yet I can command the processor to do stuff via python. LLMs can be seen as another layer of abstraction that allows us to write higher volumes of even more complex software. On the other hand, I can see how programmers can go the route of the chimney sweepers. I try to be optimistic but feel fearful as well.
Hang in there! What you can build knowing how to code is drastically different from what promptards can build. Imagine trying to build a car without knowing anything about car building - you’d just get the most generic boring clunker anyone can design.
Feel you bro, same age, same feelings. And even though AI won't replace me, the work is shit now. I like to code, not to babysit some retarded genius.
> I'm not going to go to the trades
I find it unrealistic anyway, that market will be saturated so fast, it won't make a difference for you or me, in the grand scheme of things.
My first question was “How do they know the proof correctly corresponds to the software they are checking?”
They say “ While this is an enormous volume of proof code, virtually none of it needs to be manually reviewed. The Rocq proof checker ensures that the spec is correctly satisfied by the proof. As a result, the only artifacts that a developer needs to trust are: The formal models of RISC-V and of Linux processes;
The exact theorem statements that were proved;
The Rocq proof checker itself.”
What are the formal models of RISCV and Linux? I’m guessing they allow translation of RISCV code directly into Rocq proofs?
I’d love to see more info about their workflow of code -> proof. Or even an open source tool
Exactly. How do they now that the spec that was generated was correct? Is the spec also AI generated, and could the models lie to make a spec they can verify, just like they lie to make tests pass?
It is also interesting how the LLM optimists are leaning on tools like Rocq and Lean to save them from the mess of uncertainty and confusion. These are tools created by people who understood their code and worked with deeply with type theory etc. People can keep thinking they can get away with making products from vibes, but down in the infrastructure they still have to depend on people thinking and building carefully.
It is hypocritical to campaign for "nobody will look at code anymore" while depending on the hard work of people who carefully look at code.
Model: https://github.com/theorem-labs/rocq-linux-process-semantics based on https://github.com/mit-plv/riscv-coq and Sail Binaries are split into sections with a Python script and imported into Rocq with rocq-read-file Workflow: https://theorem.dev/oss-verify/ , https://github.com/theorem-labs/oss-verify , https://github.com/theorem-labs/oss-verify-proofs
You could search “decompilation into logic.”
I've noticed that people (including myself) are becoming too lazy with LLMs.
Trying to become even lazier by skipping code reviews and then vibe-coding formal software verification will get you into trouble.
In my experience with software verification, perfect is the enemy of good. My recommendation is to start with a software design you actually understand, and then try to understand how to map your requirements to something you can prove.
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+++
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.
AGI will accelerate it, but way before agentic development I learned this was the future when I worked at Amazon. I no longer have access to the internal talks about it (amazing to watch) but here is a public link worth reading:
https://aws.amazon.com/blogs/storage/how-automated-reasoning...
You don't really need compilers anymore. LLM's can write programs over any AST and provide an equivalence proof provided you have good semantics for the source and target.
What semantics do you mean here? What are bad semantics in an interpretation/compilation context?
Semantics of a language describe the behaviour of a sentence in that language when executed. When you have semantics in a theorem prover you can construct equivalence proofs between programs expressed in different languages (or proofs that a compiler from one language to another is semantics preserving).
I was mostly referring to accuracy when I said "good" above, in the sense that they should reflect the actual behaviour of the language they describe.
Then we don't really need software anymore, LLMs can just receive every user input and perform the action required.
/s
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).
``` SELECT A, B, Sum(C) FROM Somewhere GROUP BY ALL ```
Very few developers look at the underlying “source code” that this SQL compiles into. Very few people even read the “source code” that tsc outputs.
The reality is the lowest level checkpoint worth looking at and understanding is the highest possible abstraction layer which preserves 100% of the needed precision and flexibility that the product being built requires.
Also, you’d just use something like sscache or just .o files to speed up compilation. It’d be unusual to store compiler MIR/LIR in git.
I think the important part will be figuring out what we need from the higher level language that achieves 100% of the precision and flexibility of Rust for the product being built.
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.
inform7 is closer to a dsl than a general purpose language. We might be looking at something closer to spark/ada.
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.
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.
I've enjoyed embedding declarative syntax inside imperative languages, like LINQ and prolog as a dsl. The imperative code can express temporality much easier, and the declarative code allows you to throw that away when you don't want it.
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.
I needed a chuckle and this delivered - “Typescript for SQL” gives me a mental image of a plane crashing into a train wreck.
> I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code.
This result is exactly the opposite. They're verifying at the machine code level, which is totally imperative.
I think this is indeed the direction, but am wondering is anyone actually trying it right now? Love to explore it.
I think for now the answer to adaerlangsql+++ is just Rust - but its semantics have always been about human usability.
Humans have this thing where we can only keep 7 things at once and have to juggle our context, but recall seems much more broad than model contexts.
If we were to start designing a language and toolkit based around LLM context sizes, limitations and quirks - how would that look?
Also terseness and operators are one thing, but what if it’s the other way around - English words etc - can have a much bigger vocabulary of things that can be done but can easily be generated on the fly.
For a new LLM language realistically you would need to probably either write or convert a shit ton of software to it first if you are to train an adequate model on top of it …
And also what about “IDEs” for agents? So far they are clumsily using human tools - just looking Claude string along bash loops and greps to try to eek out meaning form code _it itself had written a week ago_ is frankly frustrating.
There must be a better way and some rich agent specific tooling for code exploration and verification.
Anthropic stance has always been “yeah we tested them all, grep is better” but I still am not convinced - just by the fact that it constantly fails one or two attempts before “figuring it out” yeah it’s fast anyway but it could be _faster_ and could allow the agent to “think” in code space more and not have to validate itself at every minute step …
Rust is great! No two ways about it.
What I want tho would be Rust+Akka for example. There has to be a distributed execution mechanism that is as seamless as Java’s GC. Then the distributed execution mechanism needs to evolve to also be as light weight and “zero cost” while being seamless like Rust’s compile time memory management.
Where's the stance that "we tested them all", any links?
Buzzword salad, yummy
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.
I’m generally cautious/sceptical about the current LLM hype, but if that did ever happen and it worked to a useful degree, it might truly be a significant advance. I’m not saying that just because of the LLMs themselves, though.
To reach that point, we would first need to overcome the classic problems in this area:
1. How can you specify the required behaviour for a system in precise detail without ending up with a specification language that is essentially another programming language with similar complexity to the ones we use today?
2. How do you solve the sufficiently smart compiler problem so that producing reasonably efficient and reliable implementations of those declarative specifications is not only viable but expected?
And then, if you still need someone (let’s call them a “developer”) to carefully specify the required behaviour of the system in detail, and you also know how to reliably generate a good implementation of a specification, how much value is left for LLMs to add in this picture?
Maybe LLMs really could be trained to reliably produce good implementations in that scenario? Never say never, but it seems more likely to me that we would develop deterministic algorithms for doing so. That’s already a very hard problem that a lot of smart people have explored, but if a solution could be found, most likely it would be strictly better than relying on LLMs in this part of the process.
Maybe there would still be a role for LLMs to convert natural language problem statements into specifications? Maybe for systems that don’t really matter, that would be enough and a big time saver. However, I’m sceptical about how much time it would be likely to save for systems that did need to work, where you would still need careful design and review of all the detailed specifications by developers anyway.
Maybe LLMs would end up in a similar role to the scaffolding tools that are popular in some ecosystems today, where you feed in some basic choices and the tool then produces a first pass at the files and code you might need, which you take as a starting point for the real work but without wasting so much time on boilerplate? That seems realistic and useful, but it’s a relatively small part of what would then be the overall development process.
In short, I would love for the existence of LLMs/agents to push us towards those better programming languages and tool chains, but if that did ever happen, I wonder how much benefit LLMs/agents could still offer once developers had the more powerful languages and tools available and could work at a “higher level of abstraction” themselves.
These are the good good questions. I wish I was smart enough to answer them.
I think the best bet is to let a hundred developers play at it for a bit. There will be a lot of bespoke domain specific declarative languages. They will over time learn from each other to be better and better.
Experiments like GoogleSql’s pipe syntax https://docs.cloud.google.com/bigtable/docs/reference/sql/pi... getting pushed even further and further. That’s where I’d put my money. Cloudflare might be another candidate for building such a programming language for the distributed compute and memory “machine”.
(Also once we are there) I think there will be even better questions: What does programming CRDTs like a blockchain that reconcile across Mars and Earth look like? and in that way, LLMs will constantly be useful helpers to explore the state/latent space.
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.
i dont even think that it would be possible to build a declarative language that is flexible enough to do what an imperative language is capable of without being an imperative language itself
We don’t need “a declarative language flexible enough to do what an imperative language is capable of”
We need “a declarative language flexible enough to do what the product requires”
> 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.
Linus doesn't have to care, MirageOS already exists for OCaml, and I'm pretty sure there's something like MirageOS for Rust...
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.
Automated proofs do sound very neat but I think they'll be constrained to a vanishingly small set of already paranoid domains like cryptography, aerospace, etc. Everywhere else is going to spend the dividends on shipping more unvetted code faster, we're just trading discipline for velocity.
Llm adoption has just accelerated people's tendencies. Slop generators generate more slop. They're also finding and fixing bugs that have existed for decades. The societal incentives towards slop we will have to figure out but that's not new - for folks not on that wavelength and for when we get over that impulse at some point it's good if it can also do this. Just in general so sure does write a hell of a lot of tests. If it gets good at it this could pretty easily just become part of the agent loop and we get whatever wins we can from that.
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.
> Software doesn't have this scarcity dynamic
Time is finite. People’s problems that can be solved by software is also finite. There’s diminishing returns in improving software. Rewriting bash in rust, and then testing the result would barely help anyone. Also the real world (where inputs come from) is messy. You can have the perfect mechanism (memory safety), but that grain of sand (corrupted or unexpected data) can still make it behave erratically (wrong result).
AI is the dark energy of engineering - it pushes us further apart, faster. Some of us get pushed towards slop, others towards formal spec validation, and as time goes it will be harder and harder to see each other.
A while back a knowledgeable man was a philosopher, and they could all easily talk to each other and understand. As time went we split up - we have philosophy doctors in various fields who have very little to talk about.
This happened again when the term “engineer” fractured (even before software engineering). Software engineering itself fractured, too.
And it’s happening again now.
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.
I highly doubt this will happen.
Coz these machines process representation of knowledge, they don't process knowlegde. That part hasn't been figured out by human yet.
EDIT: typo
You’re assuming that we’re doing more than combining ideas we already know when we’re being “creative”
Sorry if this sounds rough, computer science is probably only about combination, but there are many other fields
Sorry if this sounds rough, no.
Saying that is like saying everything is about combination because well, it is even the creative stuff if you are pedantic.
The wibbily wobbly dna of humans is how we keep recombining things into new shit. Comp sci absolutely has deep creativity in it.
At least in arts, there is a true "creative" element complicated to replicate at least in the current LLMs. True artistic invention involves a "spirit of rule-breaking" that pushes culture forward. If AI is only being trained on past data, it then struggles to make the non-linear, revolutionary creative jumps we've seen throughout history.
For instance, the transition of music from the 1950s to the Beatles, then to Nirvana, hip-hop, and beyond. Before Beatles, there wasn't such thing as Beatles. Before Nirvana, there wasn't anything that sounded like that. Of course you can point out underground bands doing something like that around that era, but stray way back in time to like 1940s and chances of hearing something like Nirvana are near zero.
True art is not easy to make. It is, rather, difficult. If you lower the difficulty to make art, then it is not already a piece of art. It is just another product down the line of plenty of copy cats. Art involves risk taking that AIs I don't think are capable of producing. Art is a medium to express human emotions, and the inherent concept here is that it will end up being consumed by another human being, and it has value because you know that another human being was on the other side of the table making it. Even if you do something you consider art for yourself with an AI, the human being on the other side was, well... you. You prompted it and you guided it. I don't believe people in general would be contempt with an endless stream of autonomous AI generated stuff (if they invent such loop) because it would not only be generic, repetitive and predictable at some point, but also the fact that you know its AI it destroys the whole vibe. Same as if you get an email and you don't know if it was an AI or human behind it. If it was a human being, great, you feel a connection there. If it was AI, well... that sucks to no end, and I guess that is for a very good reason.
Although I'm using art here as the argument for creativity, I believe there may be something analogous to scientific leaps and discoveries. To my understanding, people who seem to be fairly successful in uncover the truths of the universe via science also happen to be pretty good when it comes to some artistic endeavors, even if its only about consuming and appreciating art and not necessarily creating it. So, there might be some link in creativity there. I'm open to be wrong, of course. Creativity is about risk taking and pushing the edges, not re-iterating upon what's been already there.
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/
Curry-Howard doesn't buy you any shortcuts to capability. Surely no expense has been spared in training models to write good (well modularized, robust, generic etc.) code, and yet they still write slop (poorly structured, overfit to specification gaps, etc.) We see the same sloppish habits in their mathematics, perhaps transported along the CH iso. So "train[ing] agents to write better proofs" seems to me like a grand challenge problem for AI research, just like getting them to write good code. It won't be solved just by noticing that the two problems are isomorphic: we'll keep getting models that are a little better at grinding out proofs, hence a little better at grinding out programs, but the abstraction wall won't magically drop in either world just because the same limited behaviors can be transported along CH.
The key is to make general intelligence, and train models in regimes that generalize well among many domains, rather than just a bunch of math proof tricks that don't generalize.
I think LLMs have demonstrated tons of generalization already, but I concede that being good at theorem provers don't automatically translate into being good at other forms of programming and vice versa. But the labs should probably focus on generalizing rather than optimizing for each subfield of programming individually.
Also as an aside, I meant that the use of theorem provers for proving theorems is just programming, that is, Lean, Rocq etc. are programming languages. They are functional programming languages and they invoke Curry-Howard as a reason for them to work, like, at all. And that's why their reasoning is essentially intuitionistic
You make a compelling argument, but, empirically, when you optimize code for performance, you end up with an unreadable mess that breaks all abstractions; but every time I've substantially optimized a proof for performance [of proof checking], I've ended up with better abstractions and more modularity.
That's super interesting. I wonder if you've tried optimizing for type-checking duration of a richly dependently typed program and gotten viscerally nicer code out of that.
A little before that was:
> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.
> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.
- - -
This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.
If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.
One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people
Nobody (sane) does that.
Lots of people have the implementer write the tests. But this only seems like a bad thing because of an unfortunate terminology collision:
- Microsoft culture: tests are adversarial verification.
- Google culture: tests are executable documentation.
Both of these things are important. It's really unfortunate we call both of them "tests".
At Microsoft, (verification) tests are written by a different engineer than the one who wrote the code under test. VLSI/Hardware works like this too.
At Google, (documentation) tests are written by the person who wrote the code, because it's their job to document it, and because the point of documentation-tests is to make sure other people who modify your code don't break it.
> 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.
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.
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.
This is not just plausible but in fact the most likely result.
We already have plenty of evidence of this phenomenon in programming. LLMs are awesome for working on human-written or at least human-reviewed codebases.
But when you set them loose without a human around to force them to refactor their code into something that fits in meatbag-brain-sized contexts, they drift into the ghastly nightmare of the Anthropocene (go ahead, take a look at the leaked source code for Claude Code). They can handle this for a while, especially if you're doubling your model's weight count every four months.
But when you stop doing that, they choke on their own spaghetti.
It's like Feynman said about teaching -- great theoretical physicists need to re-explain the basics to students from time to time in order to force them to come up with not just the correct physical laws, but the simplest version of those laws. Take away that constraint -- IAS or LLM -- and eventually it all goes wrong.
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.
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.
In essence this lets you verify any property you want for a given function, as long as it can be expressed as a fuzz test. Specifically, you can express your property with an assert, and then prove that it never fires. This is nice because it keeps everything in one language, rather than having to translate the whole program into Rocq and then express your desired property as a Rocq theorem.
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.
The main thing they focused on in that is just cybersecurity. Formal verification to try and get rid of surface area for vulnerabilities. Seems like a good idea idk. It also sounds like they're just kinda getting started with it - we'll have to see what opus 5.6 or 5.7 looks like after they've RLed on it a bunch
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.
Is this closed source?
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?
No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other.
Ah, interesting. I went with Ghidra p-code which seems ok but what I didn't really appreciate going in was how much of the platform API surface you have to describe before you can prove pretty much anything at all.
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
Along these lines, we used Codex to collaboratively build an alloy model for verifying the authorization model of GoodMem. After building the model, we implemented the code based on it, and, while there could be a gap in the translation process, several hours of red-teaming the server (w/attacker source code access) to try and produce a privilege escalation attack using GLM 5.3 failed.
Alloy is a tool I tried to learn many years ago, but I never learned it well enough to use it for formal verification of a complex production system. Credit goes to agentic coding tools for making it a reality.
[1] https://alloytools.org/
[2] https://docs.goodmem.ai/docs/concepts/security-model/
Reminds me of this blog post by Martin Kleppmann predicting how AI will make formal verification go mainstream
https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...
If you use LLMs to digest and summarise software maybe it can help to improve formalisation. In contrast if you use LLMs to produce more code this is contra-dictionary. More codes increases the bug surface circa logarithmically and correspondingly makes formalisation much harder as well. I want to see LLMs be used to strip away code. Only then will I believe they’re really actually good at what they’re doing.
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.
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.
That's a brutal way to do verification, at the machine code level. But it's worth it in today's threat environment.
I think it's a really illustrative example of how to play to AI's strengths. No human would dream of writing 600,000 lines of Rocq to verify one binary. The whole approach is so insane that it probably wouldn't even occur to them. But Claude has no concept of tedium, and will happily fill out lemmas all day long until the job is done. To me that's what's significant about this result: it's not about scaling up an existing technique, it's about using scale itself as the basis of a new technique.
This is of course Joseph Stalin's First Rule of LLM Assistance:
"Quantity has a quality all its own."
I believe that they chose assembly in order to diff against real projects and then see if those real projects have bugs.
I have a skill for using Verus with Rust [1]. I think they found a nice way to integrate proofs with the language. The verify skill I use lists proofs as a possible technique [2] and the project instructions have instructions on using it, but only a very small fraction of the code base I am using this on has proofs. Anyone can now have an LLM write proofs but its still difficult to know when they are more productive than other techniques and to relay that advice to an LLM.
[1] https://github.com/gregwebs/skills-sdlc/blob/main/skills/rus... [2] https://github.com/gregwebs/skills-sdlc/blob/main/skills/ver...
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?
How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.
Well they are much harder to read than tests.
I was going through an experiment trying to spec out a simple caching system in Lean. I was getting Gemini to help me run through doing this, step by step. At one point it writes out this statement with a proof to show something, the specifics of which I forget, but it was some simple property of the cache. I stare at it for a while thinking to myself this can't be right, it was some sort of plain tautological statement that didn't really say anything, like saying 1 = 1.
I give it to Opus 5.5 and it basically confirmed my gut feeling that it was useless.
I'd like to rely more on formal verification. I like the idea of starting out with specs in a formal setting and designing software that way. The problem is it's hard to do right, and my point is even with AI, it's hard to do right.
That's the nice thing about the approach described in the blog: you use the same Rocq theorem for every binary (it just says "this binary doesn't crash") and then you express the property you want in your language of choice. For example, to prove that your compression algorithm round-trips, you would write something like assert(x == decompress(compress(x))).
I fully agree it’s harder to read. I do chip design and I feel like formal is more common in this area, but I generally restrict it to very simple properties that are easy to understand without having to mentally solve a sudoku puzzle.
It’s to easy to write an assertion that looks like it checks what you want it to, and gives you a false confidence when it passes, only to figure out after a field failure that it wasn’t checking what you thought at all.
But I’d pay for a commercial set of properties and assertions that had guarantees, and not worry about their complexity. For something standard like cache protocols and bus protocols.
Other cases it needs to be pretty straightforward to grasp by a peer reviewer in minutes, or it’s not worth it.
But when you can hit the sweet spot, a set of easily understood properties (or complex but trusted properties), formal can save massive amounts of time.
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.
I mean ... The thing about formal verification is that you can write the extremely slow but correct version of your code and then have an optimizer write a much more efficient version with a proof of correctness.
For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.
If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.
Most software is ultimately like this
> 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.
One wonders how deep is Anthropic's queue of marketorials.
> 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!
> Specifically, Claude proved that these programs will always exit normally without triggering memory-safety errors or failing assertions, for every input less than 64 MB and ...
Did they solve Halting Problem?
I don't get what you mean? Granted, I didn't even try reading your message, since the language that you're using, English, is not sound, complete, decidable (or even defined).
_these_ programs not _all_ programs
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?
About time, too. I studied formal software and hardware verification “before AI” and automated reasoning and cognitive architectures were just in need of scale. People are struggling with the inherent meaningmaking of taking formalism seriously in the world. It’s easy to roll your eyes (and I do a lot of that myself) but I have a lot of sympathy. It took many years of dedicated focus for me to convince myself the validity of automated reasoning / externalized cognition.
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
I designed Sharpee and generated the code with Claude Code. About six months in I had Claude generate a manual for the language. Then I had this crazy idea of testing the manual with a completely dummy instance of Claude in a VM.
Nothing solidified Sharpee more than “compiling” this manual chapter by chapter.
But even that left gaps. I then designed a true DSL called Chord that compiles to Sharpee and this really ramped up the solidity of Sharpee.
what is sharpee. chord ?
no idea what you are even talking about
You could infer I created two programming languages or you could infer I tested AI generated constructs in a way only AI could.
I'm curious if increased adoption of formal verifications would increase migration of legacy COBOL to modern systems.
It seems like it’s a good fit. Proving equivalence is much easier than writing a spec without a golden reference.
Except COBOL systems are often easier to formally verify than modern systems.
They're often simpler, and whole classes of security vulnerabilities are mitigated by design. My favorite example is SQL injection mitigated by having proper access controls in the DB. Why prove about every SQL statement that it cannot be nefarious, when we can just prove it about the connecting user? The user access carries the intent of what the application program wants to do with the database, in a separate channel, independently of the complexity of the application.
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 you still run the risk of common-mode failure. It might be more robust to pick a different model altogether to do either the VM or the spec.
ESBMC: https://esbmc.github.io/
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 wouldn’t call them worthless. I guess it depends on the unit. But also having someone or something independently write tests is generally better than testing your own code.
If you want it to do that consistently why can't you put it in your Claude.md?
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.
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.
You do it by comparing to something that is “known” to be good.
I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.
Proving two things are equivalent is a major component of formal.
For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.
A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.
in heavy air quotes, yeah
Talk is cheap, show me the code. Claude generated a formally verified Python interpreter in Rust? Bullshit. Anthropic would have published it if they did, like that dogshit C compiler publicity stunt. That they won't even show it indicates that this is so misleading as to be a lie. They generously give themselves the grace of describing it as a "subset" of Python interpreter, and I believe them -- I can formally verify a "subset" of Python quite easily, but nobody will be impressed when they look at what that really means. Why was it tested with "1.7 million randomly generated" Python programs and not any real-world Python programs that already exist? Because the subset doesn't cover what anybody would consider to actually be Python.
Hmm? I had Claude Opus 4.6 implement a .NET compiled language that is Python-like (we already have IronPython, I wanted something Python-like that treated .NET as its entire runtime) language in about two (maybe three sessions tops?) of 1M token context windows, and the first two times I only used roughly 400 to 600k tokens? When Anthropic dropped the 1M context window update, I put it to the test.
See for yourself:
https://github.com/Giancarlos/Culebral
Anyway, my custom (currently paused because I'm taking on a much more ambitious compiler project with Claude... just to push the limits) language can build ASP .NET applications, and a bunch other things. I also took the Rust approach to types, all method signatures must have types defined, type hints are inferred when declaring new values from the value on the right.
I've also had Claude rewrite legacy C# projects with 100k+ lines of code, fully in Rust, long before Opus 5.0. I've spent the last year pushing the limits with Claude, including reimplementing existing software, which people are catching on to now, and I've managed to get rather far in some cases.
So I wouldn't be surprised if yes, Claude can implement Python, mind you, there's Python interpreter coded in Python in what was it? 500 lines of Python? You can build a Python stack machine bytecode interpreter in like 60 ~ 80 lines of Python code.
Would not surprise me if you can trim a C programming language interpreter down in terms of lines of code when you rewrite it in Rust especially when you have access to a much more functional language, not to mention Rust took the best bits out of OCaml it could to make itself very efficient at writing compilers / languages (so they could write their own compiler in Rust...).
I am also having Claude building me a much smaller compiler, which started out in under 500 lines of Python, but as I got more ambitious it had to write more code for my language, it was meant to be a slightly less restrictive Go, the Python basically converts the syntax to C which then compiles anywhere. Havent put that one on GitHub since I'm still tinkering with it.
I notice you haven't touched that repo once since the month you prompted for it. I don't doubt that you generated some cute little prototype that compiles something. I do doubt that it's something actually suitable for anybody to use for programming. My own experiments with having frontier models attempt to implement my own language have all been dire. Even with a rigorous specification and a set of hand-written programs showing both the input of my language and the asm it should output, it managed to create something that compiles exactly those programs and completely fails in real-world use beyond that. So too with Claude's own C compiler experiment; even with C's unbelievably rigorous test suites that give it a deterministic guideline and actionable feedback every time it fucks up, it was still shit. If they merely gave it a C specification, without the decades of human-written tests, there is a snowball's chance in hell it would produce anything worth using.
I think you answered your own problem: telling it what assembly you're expecting, get it to build the foundation before you start asking it how the tiles should look.
Right now I'm working on a compiler / runtime for a more complicated language than Python or C and while its "slower" I know that once it's done through this run I'll be able to have it focus on optimizations, especially with rigorous tests that some languages have to test their compilers. I have plans to run back to Culebral, but I have to scratch a bigger itch I've had, people like you who've told me repeatedly that an LLM cannot be used to build a compiler. So here I am, slowly chugging at it, getting decades of developer effort worked through every week.
If I'm wrong, so be it, if I'm right, it'll be fun to release. :)
It doesn't take a decade to write a compiler for a language. If you're putting months of your own effort into it, it's not clear that the LLM is even increasing your productivity.
I think these developments should be done with care and cognizance of the user. I worry that formalism may have trouble scaling and interacting with user intent. LLMs will (and already do in my experience) construct a formalism for your application that may be provable to some archetype -- but separate from reality and separate from your conception. The Claude user experience of rulings is already at a cultural limit among users -- the excitement over the linguistic 'improvements' of the Opus 5.5 release are a case in point. Formalism is only one axis here and usability is another. This could be a problematic development if done lopsidedly.
code changes 1000 times a day, and you want to "formally" verify it?
> “Formally verified” does not mean “bug-free.”
Is formal verification the path forward? Meh... I dont think so. Does it have applications in some areas: yes. But this is just more robust "unit testing".
Anthropic keeps trying to convince you that "one agent" will do the job. It does so with the statement "We built 36 small verification tasks from real OSS-Fuzz code. Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. We expect this trend to continue as models are trained on long verification tasks."
But this is not the path forward. Robust E2E, durable (can your app go from python to rust with out loosing tests) Simulation/Emulation tests are the way. This is an "in bulk" and "brute force" activity. Go look at TigerBeetle for an example of this in practice. Go look at how oxide is doing testing.
Can a swarm of cheaper agents write these tests more effectively that Anthropics premium products. I assure you that it can.
If you look at OAI's actions (hugging face hack) and anthropic own publication on its version control AI is not a best of breed solution its a brute force hammer at it till you get what you need solution.
> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.
I wish people would learn a little computer science before making this kind of impossible claim. And I wonder how many people read claims like this and accept them without investigation.
The Turing Halting Problem (THP) invalidates the above claim, on all nontrivial software systems, forever.
The THP (1937) is derived from Gödel's Incompleteness Theorems (1931), and the latter are not a matter of opinion.
For those with limited attention spans, ask yourself this: How does the foolproof program checker check itself?
The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.
Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
I think incompleteness theorem means that you can't guarantee the agents will always be able to converge on a proof, since you can't have both completeness and soundness (and we obviously need soundness since that's the whole point of a theorem prover).
But most real-world programs are maybe not that "expressive" since we don't even want them to be capable of infinite loops (since those would often be denial of service vectors). So you should usually be able to prove that they halt (and presumably other properties as well), especially when you allow agents to rewrite things to pull out invariants that make proofs easier (as they did).
And for cases where getting clean invariants are difficult, I imagine you can just hack it by having some cutoff which trivially ensures things always halt. (Not sure what the equivalent would be for "no bug" proofs, probably rejecting things that are technically valid input per spec but seem unusual?)
While I completely agree with 3uru, where it can get stuck is if your system contains a pseudorandom generator or some other cryptographic shenanigans. These are programs deliberately made difficult to analyze and reason about.
I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).
That's a good point, although couldn't you usually black-box those and assume the invariants we expect of those primitives are in fact true? E.g. you don't need to bother trying to prove properties about your prng itself, you can just prove how your program behaves under a random oracle model.
> The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.
No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.
> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.
That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".
> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.
The language is Turing-complete, not the program. Rice's theorem says that we can't have a program that verifies a non-trivial property for all other programs. It doesn't say we can't verify that property for some programs. That would imply you could never know anything about a program.