Hacker News read the formal verification news and asked one question: proved against what?

Anthropic's post on LLM-written proofs drew 308 comments on Hacker News this week, and the strongest thread in them is not whether the proofs hold. Almost nobody disputed that a proof checker checks proofs. The argument was about what got proved, and whether that is what anyone wanted. That is the right argument, and it is the same one AI-written tests have been losing quietly: a check is only as good as the statement of intent behind it, and when the model writes that statement too, nobody has reviewed the part that matters.

What was announced

The post, published 22 October with Theorem, describes Claude writing machine-checked Rocq proofs that 239 fuzzing entry points across 123 OSS-Fuzz libraries never crash for inputs under 64 MB. The proofs total about 180 million lines. Along the way, Claude found and patched hundreds of bugs.

The post is direct about its own limit: "a proof checker can't tell you whether your spec matches reality", and "'Formally verified' does not mean 'bug-free.'" The specs here were derived from existing fuzz harnesses, so the theorem is "this does not crash", not "this does what the user asked".

What the thread said, counted

We read all 54 top-level comments in the thread and sorted each into one stance. One reader, one pass, so treat the edges as soft. The replies under them (254 more) were read for quotes but not counted.

The first two rows together are 16 of 54, or 30%: nearly a third of the people who started a sub-thread asked some form of "proved against what?" The skeptics mostly made the same point with less patience.

The spec gap, in their words

The cleanest version came early. One commenter, woggy, wrote that even with LLM help, making the spec cover what you want is hard: "How do you actually know what the LLM proved is what you want?" A reply from y1n0 turned it on testing: "How do you know any test is checking what you want?" Their answer was the honest one: review it, and run it on things you know are good and things you know are bad.

Olscore offered the best metaphor in the thread, a house with three layers: vision, blueprint and inspection. The proofs make inspection close to perfect, "but an inspection only checks the blueprint, not our vision" (comment). paxy put it in one line: "All this is going to do is move the problem up one layer" (comment).

mentalgear went for the textbook. Verification asks "are we building the product right?", validation asks "are we building the right product?", and you "can write mathematically flawless code that highly efficiently solves the wrong problem" (comment). We wrote up that distinction, and why agents blur it, in verification vs validation.

The people using it

The practitioners were the most useful voices. sestep has been merging agent-written performance changes "because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation" (comment). That is a strong use: equivalence to code you already trust is a spec you did not have to invent. A reply from mattr03 was still the spec question: "How do you gain confidence that your theorem actually applies to your code?" (reply).

malisper reported the same pattern at scale on a Rust rewrite of Postgres: "I've proven that about 12% of the code behaves the same when executed single-threaded" (comment). The precision of that sentence is the lesson. It names the property, the fraction and the condition. A green check rarely says that much about itself.

The practical-limits camp had one line that applies well beyond proofs. m3kw9: "code changes 1000 times a day, and you want to 'formally' verify it?" (comment). Whatever checks agent-written code has to be cheap enough to re-run on every one of those changes, or it gets skipped.

Outside the thread, the same point

Write-ups elsewhere landed in the same place. Karate Labs: "A proof shows that the code matches the spec. It never shows that the spec matches what the business meant" (post). The High Learning Rate newsletter titled its summary "Claude writes proofs, but the specification still sets the guarantee" (Substack).

Back on HN, jasongross pointed at a practical way out: "the spec doesn't need to be written in a proof assistant and can instead be encoded as an end-to-end test" (comment). An executable check of the outcome you wanted is a spec most teams can already write.

The takeaway for anyone checking agent-written code

The two practitioners who were happiest had one thing in common: their spec was something they already trusted. One proved equivalence to the original function. The other proved equivalence to the original C. Neither asked the model to decide what correct means.

That is the transferable rule, for proofs and for tests. Let the model write the proof, the test, or the check. Do not let it write, unreviewed, the statement of what the change was meant to do. Write that down first, in words a person can disagree with: "one click, one charge, one order that survives a reload". Then whatever the model produces is checked against intent, not against its own guess. The proof checker closes the inspection gap. The intent gap stays open until someone writes the intent down.