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

jaykru

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

lenerdenator

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.

mjorgers

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?

pinevale

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?

pizzafeelsright

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.

yazaddaruvala

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

paxy

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?

woggy

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?

UncleEntity

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

malisper

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.

fathermarz

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.

sestep

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.

j16sdiz

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

braiamp

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

PandaRider

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

cadamsdotcom

One wonders how deep is Anthropic's queue of marketorials.

Olscore

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

passive

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.

adyavanapalli

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

operator-name

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.