FlashProve Is Not a Fact Check

2026-11-09
Brian

Subscribe
JOIN OUR NEWSLETTER
Be the first to know. Get fresh AI/Tech updates instantly, no spam, unsubscribe anytime

FlashProve is a receipt for a calculation. It is not a referee for the world.

On Sunday 2 November 2026 Anthropic published a research post, Progress on provable inference for large language models. On Monday 3 November, TechCrunch’s Russell Brandom wrote it up as a system to prove an AI model’s identity. By Wednesday morning the short version was everywhere: FlashProve proves which model answered. That sentence is real. It is also wearing the wrong coat. A proof that a particular pile of numbers produced these words is not a proof that the words are true. This page takes the coat off.

Anthropic opens with the same picture, in words: in person you can see someone, hear them, shake their hand. With a model you have almost none of that. This photograph is the 21 February 1972 meeting, from the U.S. National Archives, via It is not a picture of Anthropic. It is the check you already understand, so the missing check has something to stand next to.

If you only keep one line, keep this one. FlashProve is a receipt for a calculation. It is not a referee for the world.

A name in the window is a label

Mind map of FlashProve: commitment, proof, verifier, greedy integer, not truth
A screen label can point at a swapped model

A label is text that claims something. A badge that says “manager” is a label. The letters claude-something in an app menu are a label. Labels are cheap to copy. Anyone who controls the screen can print a different name on the same answer.

A model, here, is one kind of program: a huge list of numbers that guesses the next piece of text. Those numbers are the weights (the stored guesses, not the kind you put on a scale). The company that trained the model keeps the weights private, the way a bakery keeps a recipe private. You do not get the recipe. You get a plate, and a card that says which bakery cooked it. The card is the label.

Anthropic’s own sentence, from the 2 November post: “A user querying a model today cannot check that the responses came from the specific model that a developer claims is responding, as opposed to one secretly substituted in by a routing service for cost reasons, or even by an attacker who has tampered with the token stream.” A routing service is a middle program that picks which model to call, often to save money. A token is a chunk of text the model reads or writes, often a word or part of a word. Tampering with the token stream means changing those chunks on the way to you, after the model wrote them, or instead of letting the model write them.

Judging from the words alone does not settle which box you were in. A cheap model can sound polished. A swapped paragraph can sound exactly like the model you wanted. Quality is not identity.

Start with the calculation, not the brand

A computer follows instructions. A program is a stored set of those instructions. Most programs are rules a person wrote: if the password matches, open the door. A model is a program whose useful part is the weights. Training (the long practice run that sets those numbers) happens first, mostly once. Inference (using the finished numbers to produce an answer) happens every time you press send. FlashProve is about inference. It does not watch training. It does not watch the person who pressed send.

The model does not emit a whole essay in one breath. It guesses the next token, then the next, then the next. Each guess looks at the tokens already on the page. That is the whole trick, and it is why a proof has to be about a sequence, not about a vibe.

An abacus does not know what a sentence means. It holds digits, and a person moves them by a rule. A model holds digits, and a machine moves them by a rule. This drawing is png. It is not a diagram of Llama, and it is not a diagram of Claude.

The demo model in the post is not Claude. It is Llama 4 Maverick, a public model with about 400 billion weights. Billion means a thousand millions. You do not need the exact count to follow the rest. You need this: the proof is tied to one exact list of weights, and Anthropic showed the tying on a model they do not own, so they could talk about the list without handing you Claude’s.

The cheat, in one kitchen

Picture a restaurant. The menu says the pie is from a particular baker. Three things can go wrong, and they are different wrongs.

  1. The kitchen used a cheaper baker and still wrote the famous name on the box. That is the routing swap.
  2. The pie left the right baker, and someone swapped a slice on the way to your table. That is tampering with the stream.
  3. The right baker really baked it, and the pie is still bad. Burnt, or the wrong fruit. That is an error in the answer. A receipt from the baker does not make the fruit ripe.

FlashProve is built for the first two, and only inside a narrow set of rules I will put on the table below. It is not built for the third. A proof can be valid and the paragraph can still be wrong. That is not a footnote. That is the product.

A commitment is a wax seal, not the letter

Weights stay private; a commitment fingerprint is published

Before anyone checks an answer, the provider has to pin down which weights they mean. They cannot email you 400 billion numbers. Closed labs will not, and you would not want to store them.

A commitment is a short fingerprint of a long secret. It has two jobs, and they pull in opposite directions. Binding means that later the provider cannot point the fingerprint at a different secret. Hiding means the fingerprint does not let you rebuild the secret. A wax seal does both in the old way: the stamp says “this letter is the one I closed,” and the seal does not let you read the letter by staring at the wax.

Simon A. Eugster made this photograph on 21 October 2016. It is a stack of letters, not a model card. Source: jpg.

A new bake of the model is a new fingerprint. If the lab changes the weights and keeps the old fingerprint, the proofs for the new weights fail. That is the point of binding. It is also why “Claude” the brand and “the weights behind this commitment” are not the same name.

What zero-knowledge is asking you to believe

A proof, in ordinary life, is a reason you can check. A cryptographic proof is a reason made of math, checked by a program, so a person does not have to redo the whole job.

Zero-knowledge (often shortened to zk) means the reason does not teach you the secret. You learn that the claim is true. You do not learn the weights. Succinct means the reason is short compared with the work it talks about. A 400-billion-number recipe is enormous. A proof around 19 MB is not small for a phone, and I will not call it tiny. It is still a postcard next to the recipe. An argument of knowledge means the provider is claiming “I know a run of this exact model that produced these tokens,” and a liar is caught except with a stated, very small chance. Non-interactive means you do not have a conversation with the prover. One file arrives. You check the file. You are done.

Stack those four words and you get the name Anthropic uses: a zkSNARK (a zero-knowledge succinct non-interactive argument of knowledge). You do not need to say the acronym out loud. You need the four jobs.

This is a 2019 OSCE exercise in Bosnia and Herzegovina, from A fingerprint does not tell you whether the person told the truth. It tells you the mark matches a card you already filed. That is the shape of this proof, and it is the limit of this proof.

What actually arrives on your side

Verifier checks commitment plus proof on a CPU

Three pieces, not one magic token.

PieceWhat it isWhat it is not
The commitmentThe fingerprint of one weight list. Downloaded once, then reusedThe weights themselves
The proofA file that says “these tokens are what that fingerprint’s model would write, under the rules below.” Anthropic: about 19 MB for a request of up to 1,024 tokensA 19 MB file per word. The size they published is per request of that length
The tokensThe prompt and the reply you can readA guarantee that the reply is correct, current, or kind

The checker is called the verifier. The maker of the proof is the prover. The verifier does not need the weights, and it does not need the GPU (the graphics chip the prover uses as a math engine). The README says anyone can check with a program called cp_verify, on an ordinary CPU (the normal processor in a computer), in seconds. Anthropic’s post is more specific: on the order of 17 seconds with 24 threads, about 21 seconds on one thread. A thread is one lane of work inside the processor. I am keeping both sentences. “Seconds” is the README. “17 seconds” is the research post’s measurement, not your laptop until you time it.

A receipt is the right object. It lists what was rung up, on which register, at which time. It is tamper-evident only if tearing it shows. It is not a review of the meal. jpg. I do not know the shop.

The proof is made after the answer, in batches (groups of requests proved together). Anthropic is plain about the cost of that choice: you recompute, you wait, and the run you prove may not be a bit-identical copy of a live floating-point run. More on that in the next section. The wait is the part a chat product will feel. You can read the words immediately. You can trust the identity only when the proof shows up.

Why they did not prove all 400 billion numbers every time

A mixture-of-experts model (MoE, said like “moe”) is a model split into specialists. A token does not wake every specialist. A small gate (a tiny part that picks) sends the token to a few of them. Anthropic’s numbers for Maverick: about 400 billion weights in the building, about 17 billion in use for a given token. The prover’s work follows the specialists that actually ran, not the ones that slept.

That is the main reason a proof of this size of model moved from “a research weekend” toward “a single expensive chip can keep up with a slow reader.” It is not a reason to think every model shape gets the same speed. The post says the system assumes an MoE layout. A dense model (one that uses all of its weights on every token) is a different bill, and hiding that layout is not a goal they took on. If the shape of the model is itself a secret, this release does not keep that secret.

A catalog card is not an expert. The picture is only the selection. One drawer is the live work. The room is the 400 billion. jpg.

Greedy and integer are the words that shrink the headline

Live float or sample can diverge from the proved path

Two settings decide which calculation is even being proved. Skip them and the receipt is for a different meal than the one on your plate.

Greedy decoding means: at each step, write the single token the model scores as most likely. No dice. Sampling means: treat the scores as a stack of lottery tickets and draw one, so the same prompt can legally produce different replies. The proof Anthropic describes is about greedy decoding. A sampled reply can leave the proved path at the first token where the draw was not the top score. The proof then fails, not because the model was swapped, but because a different legal reply was the one you were shown.

Integer means whole numbers. The demo proves an integer version of the weights, in 4-bit form (each weight stored very coarsely, in a nibble, which is four bits, half of the usual small byte). The README says the real Maverick run uses a public 4-bit conversion, a 232 GB download. Floating point is the ordinary way these models do the arithmetic, with decimals, and with small disagreements between chips. Anthropic: a reply from a floating-point implementation, or from sampled decoding, can depart at some position and no longer match the computation that was proved. They also say the integer version is generally expected, and was empirically tested, to stay within a small error of ordinary floating-point inference, including the usual non-determinism of floating point. They explicitly do not extend that comfort to prompts built to force the gap. An adversary is someone trying to make you fail. Those prompts are out of the comfort sentence.

Prefill is the other word in their speed sentence. When the whole prompt is already written, the machine can score it in a wide parallel pass, instead of waiting for one new token at a time. The prover reads finished text that way. The 110 tokens a second is proof-making over finished text, not the speed of inventing the answer. Do not paste it next to a chat box’s tokens-per-second and call them the same stopwatch.

The price of the receipt

Anthropic’s comparison is against vLLM, a common open-source library for serving models. On their numbers, making the proofs costs about 70 to 95 times as much GPU time as running the model. One H100 (Nvidia’s data-center GPU; the README wants the 80 GB card, otherwise idle) produces proofs at about 110 tokens a second of prefill, when the batch holds 24 requests. A single lonely request is much less flattering. A secondary table, which

The context window (how many tokens the model is allowed to see at once) in this prototype stops at 1,024. Anthropic calls that quite short next to a real chat, which accumulates a long thread. A 1,024-token request is a few pages, not your year of conversation. Proofs of longer threads are not in this release.

Hardware, from the README, so you do not imagine a laptop prover. One H100 80 GB. x86-64 Linux. The CPU needs SHA extensions (a small hardware helper for the hash). CUDA 13.2 Update 2. A local disk. Network storage is not supported. RAM (the machine’s working memory) in their guide is hundreds of gigabytes: they cite about 280 GB for a full-size synthetic stand-in and about 330 GB for real Maverick. The verifier is the piece that is allowed to be ordinary. The prover is a small lab.

QuestionThe number they publishedThe wrong way to read it
How fast is proving?About 110 tokens/second on one H100, at 24 requests in a batch“Chat is now 110 tokens/second proved, live, on every message”
How big is the proof?About 19 MB per request of up to 1,024 tokens. A finer print in secondary coverage says 18.78 MB“19 MB per token,” which would be absurd, and is not the sentence
How much extra GPU time?About 70 to 95 times running the model on vLLM“A bit of overhead”
How long may the chat be?1,024 tokens in this prototype“It scales to the product’s context window”
Who can check?A CPU, in seconds, without the weights“You must trust Anthropic’s server to re-run it”

Prior open-source provers on this same 400-billion-weight model were far slower. Anthropic’s claim is orders of magnitude, not a few percent. One comparison that circulated with the release, again not my benchmark, puts an earlier open system, VerInf, near 0.02 tokens a second on Maverick, against FlashProve’s about 110. If that ratio is even roughly right, this week is a real change in what is demonstrable. It is still two orders of magnitude short of “free to attach to every reply.”

Two checkers, and a gap they warn you about

The repo ships more than one way to say yes.

Side channels are also out of scope, by their own writing. A side channel is a leak through something other than the message: how long the proof took, how hot the chip got, how the power meter moved. They say measuring the time to produce a proof could, in principle, say something about the weights. They are not claiming they closed that door.

This is not the September system, and it is not Claude in production

Anthropic’s Frontier Safety Roadmap had a public goal: a prototype by 30 September 2026 of provable inference, “a technique for reliably, provably ‘signing’ AI model outputs in a way that makes them attributable to a specific set of model weights.” They say they met that goal with a different project. That one signs traffic and recomputes the inference on a trusted server. Recompute means run the model again somewhere you trust, and compare. FlashProve is the other road: do not rerun the model, check a short mathematical receipt, and do it without taking the weights.

What they do list as uses, once a receipt like this exists:

HopeWhat the proof can actually supportWhat it still cannot do
A router did not quietly downgrade youIf the commitment is the model you paid for, and the rules match (integer, greedy, length), a passing proof rules out a swapped modelIt cannot see a router that never asked for a proof
A server was not rewritten under youA proof bound to the fingerprint fails if the bytes are not that model’sIt does not notice a leak through timing
“Our approved model wrote this scan”You can check the scan text against a published fingerprintYou cannot check that the finding is a real bug
A regulator wants to see which model ranA certificate per request can show the claimed weights were the ones used, without shipping the weightsIt does not show the lab trained the model safely

What to do with the headline

If you caught yourself thinkingReplace it with
“Anthropic can now prove Claude is telling the truth”They released a prototype that can prove a specific integer, greedy run of a committed weight list. The demo list is Llama 4 Maverick, not a claim about Claude’s live answers
“The proof hides everything about the model”It is built to hide the weights, aside from a declared list the README mentions. It is not built to hide the architecture
“I can turn this on in the API today”The repo says it is not maintained. The context cap is 1,024 tokens. Proving wants an H100 and hundreds of gigabytes of RAM
“110 tokens a second means it is cheap”That figure is the prover, in a fat batch, and it still costs on the order of 70 to 95 times the GPU time of serving the model
“A passed check means the paragraph is right”A passed check means the paragraph is what those weights would write under the proved rules. Ripe fruit is a different question

The people on the post, so the work has names: Roy Rinberg and Alex Allain at Anthropic; Alessandro Chiesa (EPFL, StarkWare); Miranda Christ (MIT, RESI); Rahul Dalal (Anthropic STEM Fellows, Succinct); Giacomo Fenzi (EPFL); Ben Mayer (Anthropic Fellows, MIT); Guy Weissenberg (EPFL). Anthropic also says Claude produced improvements on this kind of proof and that Claude is strong at the optimization work. A model helping build a proof about models is a good sentence. It is not a substitute for the Lean theorem.

Common questions about FlashProve

Does a passing proof mean the answer is true?

No. A passing proof means the tokens match the committed weights under the proved rules (integer, greedy, length). Truth about the world is a different question.

Can I turn FlashProve on in Claude’s API today?

The GitHub README calls it a research artifact: not maintained, not accepting contributions. The demo model is Llama 4 Maverick with a 1,024-token window, not a claim about Claude production traffic.

What did we check on this box?

We cloned anthropics/FlashProve on 9 November 2026. README reports version 0.16.0, Apache 2.0, and lean/THEOREM.md is present. We did not run the H100 prover.

JOIN OUR NEWSLETTER
Be the first to know. Get fresh AI/Tech updates instantly, no spam, unsubscribe anytime

Leave a comment