Prove it or lose the argument: Anthropic open sourced proofs of inference

Pay for frontier tokens through an API and what arrives is tokens. Nothing inside the response names the model that produced them. A routing service under load can substitute something cheaper, and the output will still read like the model you ordered, because quality is a terrible detector. Anthropic named this exact case when it open sourced FlashProve on November 2: a prototype for provable inference, Apache 2.0, code and Lean proofs public from day one.

The mechanism is a commitment plus a receipt. The provider commits to a set of weights. Every response then carries a zkSNARK, a cryptographic proof that those weights produced those tokens, and the proof itself reveals nothing about the weights. For Llama 4 Maverick, a 400 billion parameter mixture-of-experts model in 4-bit quantization, a single H100 generates proofs at around 110 tokens per second, adding roughly 19 MB per 1,024-token request.

The honest number sits right next to those: proof generation costs 70 to 95 times the GPU time of running the same inference through vLLM. That ratio is why this post exists at all. Anthropic describes prior open source proof systems as orders of magnitude slower, so the line between research curiosity and shippable infrastructure just moved.

The audit trail is the product

The build story argues for the system better than any benchmark. Claude found the optimization paths through the cryptography literature, and the post says plainly that Claude makes decisions that are hard to evaluate in something this large. So the top security claims are formalized in Lean, with an interactive visualizer for the theorems. The release includes a fast verifier in C++ for practical checks and a Lean verifier for audit-grade ones. The tool that built the system does not get to grade its own work. That instinct, applied to themselves, is the sales pitch.

What it does not cover

The scope is narrower than the headline. Proofs cover an integer version of the model under greedy decoding, contexts up to 1,024 tokens, and mixture-of-experts architectures. Sampled decoding, floating-point drift on adversarial prompts, timing side channels: all out of scope, stated in the post. Anthropic calls it intermediate progress and invites others to beat it. The repo description is blunter: "Not maintained." The market moved fast anyway. The repo topped 850 stars in the 24 hours after the Hacker News thread went up, and the thread itself collected 207 points and 93 comments in its first 14 hours.

The thread splits on schedule

The reactions ran in both directions at once. The top comment called the whole thing a stunt and implied the company pitching it understands substitution risk better than anyone. Below that, practitioners described the rumor mill around routing services quietly downgrading models under load, the exact scenario the proofs are built for. One commenter reading the repo docs noted the scheme also works for open-weight models: commit to the public weights, publish the seed, and anyone can recompute the commitment themselves. The full thread is worth the scroll for anyone selling model access.

Who pays the surcharge

A 70 to 95 times compute premium only makes sense where the product is trust. Evaluation labs need to know the model they tested is the model that ships. Regulated clients buying through a router want the receipt attached, and providers selling compliance-sensitive tiers can price verification in. My rule of thumb after reading the cost table: nobody bolts this onto commodity inference, and nobody needs to. Trust sold as a feature pays the bill; commodity inference keeps running unproven.

The router rumor mill, where providers get quietly accused of downgrading models under load, now has a technical endgame: prove it or lose the argument. The 19 MB attachment makes a strange kind of invoice. It is the first one that itemizes the weights.