Which Model Actually Answered You? Anthropic Open-Sources FlashProve, a zkSNARK That Proves Inference at 110 Tokens a Second

Anthropic’s research post “Progress on provable inference for large language models” is dated 2 November 2026; most of the press picked it up on 3 November. It introduces FlashProve, an open-source system that lets a model provider prove, with a cryptographic proof rather than a promise, that a given reply was produced by one specific set of model weights. The weights stay secret. The person checking needs no GPU.

The headline numbers come from the post and the 23-page technical report, and they are the reason the release is worth a close look. On one NVIDIA H100, FlashProve generates proofs for Llama 4 Maverick, Meta’s 400-billion-parameter mixture-of-experts model, at about 110 tokens per second. Each proof is 18.78 MB and a 24-core CPU verifies it in 17 seconds. The only earlier proof of the same model that Anthropic knows of, an open project called VerInf, took 14.3 hours to prove 1,000 tokens on a DGX Spark and produced a 93.6 GB proof that needed almost a day to verify.

What was released

Five artifacts, all under Apache 2.0:

the blog post itself;
a technical report, written by the human authors: Roy Rinberg and Alex Allain of Anthropic, Alessandro Chiesa (EPFL and StarkWare), Miranda Christ (MIT), Rahul Dalal (Succinct), Giacomo Fenzi and Guy Weissenberg (EPFL), and Ben Mayer (MIT);
a much longer protocol specification that was written by Claude and that the authors say they “did not review in detail”, with a carefully reviewed paper promised later;
executable code in the anthropics/FlashProve repository, version 0.16.0: a GPU prover, a fast verifier in C++, and a slower verifier written in Lean;
Lean proofs of the top-level security statements, plus an interactive visualiser of the theorems for auditors.

The README is unusually blunt about status. The repository is “a research artifact: not maintained, not accepting contributions”, and the known-limits page says AI systems under human direction wrote nearly all of the software, the Lean proofs and the documentation, and ran the reported tests. TechCrunch reports that there are no plans to deploy the system at Anthropic or any other lab. Anthropic itself describes the post as “intermediate progress, and not a completed research agenda”, shared “with the goal that others look at what we have done, take it, and improve it”.

The problem it attacks

When you call a model through an API, you see tokens. You do not see which weights produced them. A routing service can quietly swap in a cheaper model to save money. A benchmark operator can swap in a more expensive one to inflate a score. An attacker who compromises an inference server can tamper with the token stream while hiding among genuine responses. Anthropic adds a case that only a frontier lab would list: as models become capable of improving and deploying themselves, “a more advanced model could run in place of the one that was authorized and present itself as the weaker model, so as to avoid the classifiers and monitoring that would apply to it.”

That last line is not abstract for this company. The day before the post, Anthropic’s amended IPO filing told the SEC it “may imminently meet” its Responsible Scaling Policy’s definition of “dramatically accelerated progress attributable to AI”, which this blog’s earlier coverage of the S-1 did not yet contain. FlashProve is pitched as one piece of the tooling such a lab would need to know which weights are actually running on its own servers.

The post also ties the work to a public commitment. Anthropic’s Frontier Safety Roadmap promised “a prototype by September 30, 2026 of provable inference”. A footnote explains the fine print: the commitment was met by a separate project that signs inference traffic and recomputes it on a trusted server, and the 19 October RSP update renamed the goal to “inference verification” because “provable inference” suggested a narrower approach than the company now thinks is needed. FlashProve pursues the same objective by a different, software-only method.

How it works, in developer terms

FlashProve is a zkSNARK, a zero-knowledge succinct argument of knowledge, built the way modern hash-based proof systems are built: an interactive oracle proof (IOP) is compressed with Merkle commitments and then made non-interactive with the Fiat-Shamir transform. The only cryptographic assumption is that the compression function inside the BLAKE2 hash behaves like a random function. No elliptic curves, no trusted setup, and plausible post-quantum security. The report says the same recipe runs production rollups such as Starknet.

Operationally there are two phases:

Commit (offline, once per model). The provider encodes the weights, hashes them into a short commitment, and proves the encoding is well formed. For Maverick this takes about 39 minutes and the provider stores 2.15 GB. The commitment is good for roughly 16 million requests before it must be regenerated. The client downloads about 6.5 MB once.
Prove (online, per request). For each reply the prover shows that the committed model, run on this prompt, produces exactly this token. Each request is a 1,024-token window and each proof certifies one token, the model’s greedy choice after the prompt. The prover batches up to 64 requests, opens the weight commitment once per batch, and emits one 18.78 MB proof per request.

Three engineering decisions explain the speed. First, the prover’s work scales with the experts that actually fired, about 17B of Maverick’s 400B parameters per token, while the proof still hides which experts were chosen. Second, proving is post-hoc: finished text is re-read in one parallel pass, the way prefill works, rather than token by token like decode. Third, the system fits on one 80 GB GPU by keeping the 232 GB of 4-bit weights in roughly 290 GB of host RAM and streaming them in a segment of layers at a time.

The cost is spelled out. Against vLLM running the FP8 release of the same model on eight H100s, proving a batch of 24 requests takes about 72 times longer per GPU than plain prefill (66 to 77 across runs), and about 94 times longer than vLLM at the highest load tried. A single request proved on its own is ready in 58 seconds, but throughput drops to 17.6 tokens per second. In a batch, an individual request waits about five minutes for its proof.

The security bound in the README is concrete: a dishonest provider is caught except with probability about q/2^124 + 2^-101 after q hash queries, for a 128-bit security target.

Formal verification, and where it stops

The team’s own framing is that Claude is good at optimisation “but often makes decisions that are hard to evaluate, especially in large complex systems”. Their answer is to state the protocol and its three properties, completeness, soundness and zero knowledge, in the Lean proof assistant, so a reviewer has to check that the theorem statements match the intent rather than audit thousands of lines of cryptographic code.

The report is careful about what this does and does not buy you:

Soundness depends only on the verifier. The executable Lean verifier is proven to accept only what the soundness theorem accepts. The fast C++ verifier “carries no formal guarantee”; it agrees with the Lean one on every proof in the tests, which is testing, not proof.
The GPU prover is C++ that an AI agent generated from the Lean representation, with no proof of equivalence. A bug there can break completeness or leak weight information, but cannot forge a proof.
Zero knowledge is formally proved only when requests are proved one at a time, not yet for batches, which is the mode that reaches 110 tokens per second.
All proofs live in the random oracle model. That is standard applied cryptography, but it is a heuristic, not a theorem about BLAKE2.

How it compares

The post’s prior-work section doubles as a short history of zkML. ZKML in 2024 proved GPT-2 at about 0.006 tokens per second; zkLLM the same year reached roughly 2.5 tokens per second on LLaMA-2-13B in batch on an A100; DeepProve, a current peer-reviewed system, reports 2.9 tokens per second on GPT-2 and 31 distributed; VerInf, on Maverick, managed about 0.02. The nearest commercial comparison is Attestable, which reports 53 to 77 tokens per second for the dense 31B Gemma 4 on one H100 but has released no code. FlashProve’s claim is therefore two things at once: a jump of several orders of magnitude on a model 30 times larger than most prior academic targets, and the first open implementation at that scale.

Anthropic’s own reading is that an overhead of “roughly 2 orders of magnitude” over native inference is “much less than previously expected”, and that this should transfer to other architectures. That is a forecast, not a result.

Why it matters

For developers the near-term relevance is the routing problem. Aggregators and gateways already front a large share of API traffic, and claims that some degrade or substitute models have been circulating for a year; Anthropic’s post links to Moonshot’s Kimi “vendor verifier” as an example of the current, statistical approach. A proof attached to each response would turn “trust the router” into “check the proof”, and the check runs in seconds on a laptop with no weights. The same mechanism gives independent evaluators a way to know that the model they tested is the model being served.

For regulators and for the pacing debate, the pitch is that proofs let a provider demonstrate that its hardware served the committed model during a period, without handing over weights. The post is honest that this proves inference happened, not that training did not happen on the side.

For the labs themselves, the tamper-detection case may be the strongest. A proof bound to a commitment detects a compromised server, or a model that substitutes itself, without trusting the server. Post-hoc proving cannot prevent a bad response from reaching a user; it guarantees the tampering is caught later. The report positions this as defence in depth, alongside trusted execution environments, which it treats as complementary rather than competing.

Open questions

Scope. 1,024-token contexts are an order of magnitude or two short of chat reality. Each proof certifies one token under greedy decoding of an integer-quantised model; a sampled, floating-point response can legitimately diverge, and the report defers to statistical methods to separate benign drift from tampering. The MoE architecture is visible, which a provider might consider proprietary.
Cost. Seventy to ninety-five H100-seconds of proving per H100-second of inference is a large bill at any real traffic volume. The obvious deployments are sampling a fraction of traffic, or proving on demand for high-stakes requests, not proving everything.
Assurance. Nearly all of the code and proofs were AI-written; the detailed protocol document is unreviewed; there has been no independent security audit; side-channel attacks on the prover are out of scope. The Lean statements are the thing to audit, and Anthropic is asking the community to do exactly that.
Adoption. A research artifact that is “not maintained” from a lab with “no plans to deploy” is an invitation, not a product. Whether routers, evaluators or regulators pick it up is the question the next year will answer.