FlashProve proves which model answered, at 70x to 95x the GPU time. Where verifiable inference pays

Anthropic released FlashProve this week under Apache 2.0, and it lets a provider attach a cryptographic proof to each reply showing which committed weights produced it. If you pay for a model through an API, that is the first practical answer to a question you could not settle before: did you get the model on the invoice? A provider under load could quietly route you to a cheaper model, and from the outside the only evidence is a vague feeling that answers got worse. By the published figures, each proof costs roughly 72x to 94x the GPU time of normal serving.

What it proves

The protocol has two steps. The provider publishes a commitment that binds it to one set of weights, a fingerprint that reveals nothing about the values. Then, for each reply, its GPU produces a zkSNARK proof that the committed model produced those output tokens. Anyone holding the commitment, the prompt and the reply can check the proof on an ordinary CPU, without the weights.

According to Help Net Security, the work comes from Anthropic's Frontier Red Team with collaborators at EPFL, MIT and StarkWare. The repository includes the CUDA prover, a fast C++ verifier, and a deliberately slow reference verifier in Lean, where the protocol's completeness, soundness and zero-knowledge properties are proved.

The numbers

Follow one request through it. The only model demonstrated is Llama 4 Maverick, a 400B mixture-of-experts model with about 17B active parameters per token, proved on a single 80 GB H100 backed by about 290 GB of host memory. Before serving anything, the provider spends about 39 minutes committing to the weights, once, and you download a 6.5 MB commitment, once. Then you send a 1,024-token request. The prover works through it at about 110 tokens per second and hands back a proof of about 18.78 MB. Your side checks it in about 17 seconds on 24 CPU threads, or about 21 seconds on one, so the check fits on an ordinary machine and the expensive part sits entirely on the provider's GPU.

The baseline matters. Overhead is measured against vLLM serving the same model in FP8 on eight H100s: about 72x per GPU on average and about 94x at the heaviest load tested. So if a reply costs you one cent of GPU time today, a proven reply costs somewhere near a dollar, before you store almost 19 MB of proof per request.

Verifiable inference is real now. It is priced for audits, not for chat.

What it does not prove

The repository's known-limits page is unusually blunt, and I trust the project more for it. Proofs are about an integer model, quantized and fixed-point. How closely that tracks the floating-point model you would normally serve "is a measurement, not part of any proof", and in one measurement the top token differed at 6.81 percent of positions. The context limit is 1,024 tokens. Interesting Engineering reports that it covers greedy decoding only, so sampled outputs at normal temperatures fall outside it.

The subtler point: the commitment binds the provider to some weights, not to a named model. The limits page says plainly that the provider chooses the model and can commit to any model it likes. A proof tells you every reply came from the same committed weights. Someone still has to vouch that those weights are the model on the price list, for example a third party computing the commitment from published open weights.

There is more. Soundness is machine-checked only for the Lean verifier; the C++ verifier and the CUDA prover are tested against the protocol, not proved. There has been no independent security audit. The page also states that AI systems, under human direction, wrote nearly all of the software, the Lean proofs and the documentation. The README calls the repository a research artifact that is not maintained and does not accept contributions. I read these Lean-backed claims the way I read Claude's proofs for 123 libraries: the theorem is only as useful as its assumptions.

When it makes sense, and where it is dead for now

It makes sense where volume is low and a dispute is expensive. A regulator spot-checking which model a provider serves. An evaluation lab that wants to prove a published benchmark ran against the claimed weights. A contract with an inference vendor that lets the customer demand proofs for a random sample of requests, say one in ten thousand, so the overhead lands on a tiny fraction of traffic while substitution stays risky for the vendor. Random sampling is the economic trick here: the vendor never knows which reply will be audited.

It is dead for now in interactive products, anything past 1,024 tokens of context, sampled generation, and closed frontier models served in floating point. It also does nothing for local inference, where you already know which weights you loaded; there, verifying your downloads is the cheaper control.

If you buy open-weight inference from a third party, put one question on the agenda of your next vendor call: will you support FlashProve or something like it, and when? Then take the answer into the contract renewal as a clause that lets you demand proofs for a random sample of requests once a production-grade prover exists. A vendor that signs is betting it serves the weights it bills you for. A vendor that changes the subject has told you how seriously it takes model substitution, and you found out before you ever needed a proof.