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.

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.

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

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

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.

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

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 is really cool work. The particular spec structure/methodology does seem awkward though:

1. Prove the ASan-instrumented binary doesn't crash

2. Prove the non-instrumented binary doesn't crash

3. Prove the instrumented and non-instrumented binaries have the same behaviour (under a particular model of a Linux process's behaviour)

This is a clever hack for automatically generating a formal spec for an existing program, but the fact that you need ASan in there makes it seem like this is less general than it sounds. Could the agents directly prove that out of bounds memory accesses don't occur on the original binary and skip ASan altogether? It's convenient to let the spec just be "it doesn't crash", and ASan provides a crash when the other bad things you care about happen (i.e. out of bounds memory accesses), but I wonder if modelling the memory accesses directly would simplify things.

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.

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.

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/

Re: footnote 5

> This technically also means we have to trust the hardware, OS, OCaml compiler that the Rocq proof checker relies on.

It just so happens Claude and I recently did an independent implementation of OCaml and ruled out malware in the compiler bootstrap via DDC (and also by achieving byte identical outputs).

https://discuss.ocaml.org/t/ocaml-compiler-implemented-in-c-...

So, we can at least rule out "trusting trust" malware in the OCaml part of the stack and up. (Rocq does not have trusting trust concerns since it's implemented in OCaml and C)

This is exactly the kind of stuff I am slowly realising with the increased adoption of agentic runtimes in enterprise SaaS products.

We will move into formal verification alongside AI tools, thus generation of executables via translation to 3 GLs is going to be a transition step, just like Assembly coders wary of optimising compilers always wanted to manually check the generated Assembly code.

And yes, many of us will have to search another source of income as an outcome of "progress".

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.

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.

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?

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

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!

I'm a dumb guy, so please excuse me in advance, but how do you verify the verification code is doing what it says its doing (verifying). If the answer is "another verifier" - how many turtles do you need to make this work?

That's a brutal way to do verification, at the machine code level. But it's worth it in today's threat environment.

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'm studying coding these days, and I thought I should still be able to read code, but I'm starting to wonder if I really need to read it, and then what I should do.

Getting tiring to read everyday in hackernews about shovels sellers telling us their shovels are so good at finding gold.

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 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 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'm curious if increased adoption of formal verifications would increase migration of legacy COBOL to modern systems.

I think the hard part of formally verifying something is not writing code. Granted it is hard and LLMs will help with that.You also need to model the user space correctly and this is a bit like causal modeling, there are many confounding factors to be taken into account and if you missed something at modeling time you'll miss bugs

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

Big fan of sel4 for this.

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.

> The Linux kernel—one of the most well-tested pieces of software today,

I feel like these people aren't really experts in the field of testing... Linux is not known for its testing... there's plenty of good things one can say about Linux, but great testing isn't one of those.

Now, things that are well-tested are things that do critical stuff, like avionics, power-plant control, medical equipment, storage... It's software from a different league.

Linux is too big, too dynamic, too distributed between different authors to hope for great testing. And it's OK. I'd rather have more people being able to contribute, not being constrained by the difficulties of the testing than have a very well-tested and borderline useless system.

A probabilistic technology (yes I know you can set the temperature to 1, but no one does that, and the output is still not efficiently predictable) is doing "formal verification" now?

Or are they just saying we can use LLMs to generate a piece of code/test that can do formal 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?

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.

But how do you guarantee that LLMs do not lie?

I was thinking about addressing the issues mentioned (multiple times before, but most recently) a couple days ago by a Facebook employee who was scared of releasing code that nobody understands.

I see two possible ways forward, not necessarily mutually exclusive.

* Make AI work with languages with reduced complexity. A lot of language complexity exists to make it (surprise!) easier for humans to deal with the language. For example, generics in a language like Java make it easier because they allow the programmer to write many similar programs just once. And because people are prone to make mistakes when working on repetitive code, generics are useful for people. AI, on the other hand, doesn't get tired. It doesn't care if it needs to implement the same template for a different type a dozen more times. So, if we give AI a language without generics, it will be just as happy, but it will eliminate a whole class of potential errors related to eg. up/down-casting of generic collections. Similarly, we could remove "dangerous" tools like infinite loops, or outlaw some system calls, producing less generic / more purpose-built languages (like PostScript!) Perhaps projects like OMeta could see some revival in this light?

* Replace, as much as possible, the work of testers with proofs, but not AI-generated proofs! The formal specification (which is another way to look at the proof, at least its statement) is where the human being needs to provide input to AI. If it's not possible to read the whole generated code, we need a tool more reliable than a test to convince ourselves that the code does what we want. Formal verification, or, even better, tests generated dynamically from formal specification (there's no need for AI to do that, this can be an entirely deterministic process) should be the way for the human to stay in the loop.

I wondered how they come up with the specifications. It turns out that they cheat yet again, take existing test suites (probably with horrible coverage) and prove that some new code satisfies the tests and does not crash.

People, hide your test suites from the criminals.

If it is formal, you don't need LLM.

If you need LLM, it is not formal.

Formal software are not LLMs.

LLMs/agents can use formal software.

The limit of formal software is the formal model itself, roughly speaking the binary specification is designed by humans. If the formal model is "wrong", bravo, you have formally proven a "wrong" model...

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

code changes 1000 times a day, and you want to "formally" verify it?

in heavy air quotes, yeah

> “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]

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