Table of Contents
Anthropic has released FlashProve, an open-source research prototype that lets users verify that an AI output matches a specific model without accessing its weights or running the model themselves.
The system uses zero-knowledge cryptographic proofs to connect an output to a fixed set of model weights. That could let customers check which model a routing service actually supplied, help evaluators verify the model under examination, and expose responses altered by a compromised inference server.
In Anthropic’s tests on Meta’s Llama 4 Maverick, FlashProve processed about 110 tokens per second on a single Nvidia H100 GPU. That figure measures proof-generation throughput over completed text, not the speed of generating new answers. Each proof checks one output token against a context window of up to 1,024 tokens, producing an approximately 19 MB file that a CPU can verify in seconds.
Anthropic’s Frontier Red Team published the work with researchers affiliated with EPFL, StarkWare, MIT, RESI, and Succinct. Anthropic credits Claude with producing improvements to the underlying proof system and finding new ways to combine existing cryptographic techniques.
How FlashProve Binds an Output to a Model
FlashProve separates verification into two stages. First, the provider publishes a cryptographic commitment, a compact fingerprint that binds it to one exact set of weights while keeping those weights hidden. Later, it produces proofs connecting requested computations to that commitment.
A verifier needs the commitment, the input, the claimed output, and the proof, not the model weights. The check establishes that the committed model, evaluated under the protocol’s specified arithmetic and decoding rules, produces the checked token.
The commitment must also identify the model the user intended to check. FlashProve’s documentation instructs users to obtain its identifier from a trusted party, rather than accepting an identifier supplied by the same server whose response they are verifying. Otherwise, a server could supply a valid proof for a different model.
The cryptographic construction is a zkSNARK, short for zero-knowledge succinct argument of knowledge. “Zero knowledge” means the proof does not disclose the private weights, intermediate computation values, or which expert subnetworks processed a token. “Succinct” means checking the proof requires much less work than repeating the model computation. The model architecture itself is not hidden.
The technical report describes a hash-based construction. It begins with an interactive oracle proof, which allows a computation to be checked through a small number of queries. Merkle commitments bind the prover to the underlying data, and a technique called the Fiat–Shamir transformation replaces an interactive exchange with a single proof file. Anthropic says the hash-based approach offers post-quantum security.
FlashProve generates proofs after inference rather than alongside each newly generated token. It reads finished text in a parallel pass, similar to an inference engine’s prefill stage, when the model processes an existing prompt. This lets providers batch requests and share some proof-generation work, with verification arriving after the response.
What the Performance Results Measure
The evaluation used a public, third-party 4-bit conversion of Llama 4 Maverick, a mixture-of-experts model with roughly 400 billion total parameters and about 17 billion active per token. Mixture-of-experts models route each token through a subset of their networks rather than using every parameter.
FlashProve exploits that sparsity, so the prover’s per-token work scales with the experts that actually ran, while the proof hides which experts were selected. To fit the workload on one 80 GB H100, it keeps weights in host memory and streams them to the GPU in segments. The reported setup uses about 290 GB of host memory alongside the GPU.
| Measurement | Reported Result |
|---|---|
| Initial model commitment | About 39 minutes on one H100 and 24 CPU cores |
| Commitment lifetime | About 16 million requests before recommitting |
| Online proof-generation batch | 24 requests in about 223 seconds |
| Aggregate prefill proving throughput | About 110 tokens per second |
| Proof size per request | 18.78 MB |
| Commitment download | About 6.5 MB |
| CPU verification | 17 seconds on 24 threads, or 21 seconds on one thread |
Proving remains substantially more expensive than ordinary inference. Anthropic compared FlashProve with an FP8 version of Maverick running through vLLM on eight H100s. Normalized per GPU, proving took about 72 times as long at the same batch size and about 94 times as long at vLLM’s highest tested load. Those figures are the basis for its roughly 70-to-95-fold overhead estimate.
Where Formal Verification Applies
Anthropic used the Lean proof assistant to formalize the protocol and its security properties. These cover completeness, meaning honest proofs are accepted; soundness, meaning false claims cannot feasibly pass verification; and zero knowledge, meaning the proof does not expose the protected model information.
Those statements rely on a mathematical model of the hash function known as the random oracle model. They also need to describe the intended inference computation accurately, which is why the release includes an interactive viewer for auditing the formal statements.
The release contains two executable verifiers. A slower Lean verifier has a formal connection to the soundness theorem, subject to trust in the Lean compiler. The faster C++ verifier has no equivalent formal guarantee, although Anthropic says both verifiers agreed on every proof in its tests.
The distinction also affects weight privacy. The mathematical zero-knowledge guarantee depends on the prover implementing the specified protocol correctly. Anthropic has not formally established equivalence between the fast executable code and the Lean specification, and providers handling private weights would need to audit that implementation.
What Developers Can Use Today
FlashProve proves an integer version of the model under greedy decoding, which selects the highest-scoring next token. Outputs from floating-point implementations or sampled decoding can differ from that exact computation. Its current context limit is 1,024 tokens, and its efficiency relies on mixture-of-experts architecture. Timing and other side channels fall outside the protocol’s privacy guarantee.
Anthropic identifies potential uses in detecting model substitution, verifying that a particular model analyzed text or code, and checking whether providers serve approved models. It also proposes using inference proofs to support oversight of compute allocation. Such proofs can establish that specified inference computations occurred, but do not establish that hardware was not also used for training.
The FlashProve repository includes the prover, both verifiers, a protocol description, Lean proofs, and examples under Apache 2.0. Anthropic labels it a research artifact that is not maintained or accepting contributions. The model weights are a separate download governed by Meta’s Llama 4 license.
Developers can begin by building the CPU verifier and checking a supplied proof for a small synthetic model, without a GPU. Reproducing the full Maverick example requires the H100-based setup and access to the separately distributed weights and tokenizer.
