You call an API and pick a specific model — but there is no way to confirm the reply was actually produced by that model. A routing service could silently swap in a cheaper one, or an attacker could tamper with the token stream, and output quality alone cannot tell the difference. Anthropic's newly released research offers a cryptographic answer: FlashProve, an open-source prototype that uses a zkSNARK (a zero-knowledge succinct argument) to turn "this reply came from the committed set of weights" into a machine-checkable fact (research post).
The numbers first
All figures below are from Anthropic's own report. The test subject is Llama 4 Maverick: a 400B-parameter mixture-of-experts model, roughly 17B parameters active per token, 4-bit quantized (about 232 GB). The hardware requirement is a single H100 plus 24 CPU cores: proofs are generated at about 110 tokens per second, and each proof file covers a 1,024-token request at about 19 MB. Verification needs no GPU — 17 seconds on a 24-thread CPU, or 21 seconds on a single thread. The cost is compute: proving takes roughly 70-95 times the GPU time of running vLLM directly. A one-time offline commitment to the weights takes about 39 minutes and covers around 16 million requests. The technical report, protocol spec, executable code and Lean proofs are all released under Apache 2.0 (GitHub repo, currently a single initial commit).
Why it is fast
Three engineering decisions stand out. First, MoE structure: proving work is proportional only to the experts that actually ran — the ~17B active parameters, not all 400B. Second, post-hoc batch proving: finished text is proven in one parallel pass, and the weight commitment is opened once per batch instead of once per request. Third, a single-GPU design: weights are streamed in segment by segment, so one 80 GB GPU with about 290 GB of host memory suffices. For context (numbers also from Anthropic's survey): zkLLM in 2024 proved a 13B model at about 2.5 tokens/second; VerInf, the only prior system to prove the same Maverick model, ran at about 0.02 tokens/second — 14.3 hours for 1,000 tokens with a 93.6 GB proof. FlashProve reaches 110 tokens/second on the same model with 19 MB proofs verifiable in seconds. Anthropic says it is substantially faster than prior open-source systems; the commercial vendor Attestable has reported 53-77 tokens/second on a 31B dense model but has not open-sourced a library.
What it does not claim
Four hard limitations are stated openly. The proof covers an integer-quantized model under greedy decoding — floating-point implementations or sampled decoding can depart from it. Only the weights are hidden, not the architecture, and the system currently assumes a MoE model. Context is capped at 1,024 tokens, far from real chat sessions. And the fast C++ verifier itself carries no formal guarantee — what Lean proves are three protocol-level properties (completeness, soundness, zero knowledge); auditing that the C++ code matches the proven protocol remains manual work. The system also only proves that hardware is genuinely serving the committed model — it cannot rule out training happening on the side.
Who actually needs it
Regulators and auditors are the first customers: pacing-style oversight could require providers to hand over inference certificates for a given period, checkable without learning anything about the weights. Second, tamper detection: a compromised inference server, or a stronger model impersonating a weaker one, cannot produce valid proofs for the expected weights. Anthropic's Frontier Safety Roadmap had publicly targeted a provable-inference prototype by September 30, 2026. Third, provenance: independent evaluators finally get a technical handle on whether the model tested before release is the model being served after.
The most interesting part of this release is not the throughput but the division of labor. Anthropic states plainly that Claude did the optimization, that Claude's optimization decisions are hard to evaluate, and that this is exactly why the top-level security statements are written in Lean, machine-checkable. AI writes the code; formal verification signs off on it. That pattern may outlast the 110 tokens-per-second headline. Once model outputs can carry a cryptographic receipt, how long can the quiet model-substitution business survive?