Anthropic published research on FlashProve on 2 November 2026, describing a way to check that an AI reply came from a particular version of a model without exposing its weights. Developed by its Frontier Red Team with researchers from EPFL and MIT, the system addresses a problem for people using hosted models: a convincing answer alone cannot tell them whether the model they requested produced it.
Key points
- FlashProve uses cryptographic proofs to tie a reply to committed model weights while keeping those weights hidden.
- Anthropic reports proof generation at around 110 tokens per second on one H100 GPU for Llama 4 Maverick.
- Anthropic says proving takes approximately 70 to 95 times the GPU time of running the model on vLLM.
- The released code and formal proofs are research artifacts with limits on the computations they cover.
FlashProve ties replies to committed weights
The method begins with a commitment to a specific set of model weights: a cryptographic identifier that can be shared without handing over the weights themselves. For a prompt and its reply, FlashProve then produces a zkSNARK, a compact proof that another computer can check against that commitment. The check is intended to fail if the reply differs from the output of the committed model. It is rather like checking a seal against an identified package, except that the contents remain closed and the proof concerns the computation that produced the answer.
Checking whether a paid-for answer came from the promised model could therefore become possible without seeing its weights or running it again. If the answer came with the proof and commitment, its origin could be checked independently of how persuasive the words themselves sounded.
Anthropic identifies independent model evaluations and requests sent through third-party routing services as possible uses. In either case, the relevant question is whether the system that answered was the one selected, rather than whether the answer was good. The company says the commitment and proofs conceal the weights, while the model’s architecture is outside FlashProve’s hiding goal.
FlashProve also conceals which subnetworks of a mixture-of-experts model handled each token. Such a model has many sets of weights but activates only some for a given token. For Llama 4 Maverick, the proving work follows roughly 17 billion active parameters per token rather than all 400 billion, Unite.AI reported. That distinction matters to fitting proof generation onto the hardware Anthropic tested.
One H100 produces proofs at 110 tokens per second
Anthropic tested FlashProve on Llama 4 Maverick, a 400-billion-parameter mixture-of-experts model, using 4-bit quantised weights and integer arithmetic in the prompt-processing phase. It reports that one H100 GPU generated proofs at around 110 tokens per second. Those conditions matter: the reported speed belongs to that model, numerical representation and computation, rather than to every way of serving a model.
Anthropic puts the proof size at approximately 19 MB for a 1,024-token request. It says proof generation used approximately 70 to 95 times the GPU time required to run the model itself on vLLM, an open-source library for serving models. The comparison separates the ability to produce a proof on one GPU from the cost of doing so alongside ordinary inference.
Unite.AI gives the proof size as 18.78 MB per request and reports about 72 times the per-GPU time of vLLM for the same batch, rising to about 94 times at the highest vLLM load tested. It reports that 24 requests took about 223 seconds to prove using one H100 and 24 CPU core units. The commitment stage, which takes place before individual replies are proved, took about 39 minutes in that account.
Checking a completed proof requires no GPU. The reported verification times were 17 seconds using 24 CPU threads and 21 seconds using one thread. That places the expensive computation with the party producing the proof, while allowing a separate party to check the result on a CPU.
Lean proofs accompany the FlashProve code
Anthropic released executable code for a prover and two verifiers, one written in C++ and another in Lean, a language used to express and check mathematical proofs. The release also includes a technical report, a protocol specification, Lean proofs of top-level mathematical statements and an interactive aid for examining those statements. The code, proofs and documentation carry the Apache 2.0 licence.
Anthropic describes the work as intermediate progress rather than a completed research programme. The distinction between the verifiers matters for anyone building on the release: the Lean verifier is formally connected to a soundness theorem, while the faster C++ verifier was tested for agreement with it, according to Unite.AI. Formal statements also require human review to judge whether they express the intended security guarantees.
Unite.AI reports that the proofs cover exact integer weights under greedy decoding, in which the model selects its highest-ranked next token. Floating-point inference or sampled decoding can produce a different computation, and the covered context is limited to 1,024 tokens. It also reports limited testing against adversarial proofs and weight-hiding attacks, no independent security audit, and a repository labelled version 0.16.0 that describes itself as an unmaintained research artifact not accepting contributions.
