LLMs are making formal software verification feasible at a much larger scale

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.

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.

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.

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

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+++

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.

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...

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?

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.

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...

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.

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.

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 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...

is it just me, or is Anthropic posting more articles like this (and similar other topics) in the past few days than before? And more of them are ending up in HN front page?

If I recall correctly the only news they used to post were new models updates, while now they have expanded their topics, or so I feel.

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?

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?

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!

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

> 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?

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

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.

I'm curious if increased adoption of formal verifications would increase migration of legacy COBOL to modern systems.

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.

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?

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.

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.

[flagged]

[flagged]

[flagged]

[flagged]

[flagged]

[flagged]

[dead]

> 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?