THE ESSENTIALS IN 30 SECONDS

  • FlashProve generates a zero-knowledge proof that a given set of committed weights, run on a prompt, produced the returned tokens, while keeping the weights hidden.
  • On Llama 4 Maverick (4-bit) and a single H100, it proves about 110 tokens per second, with proofs of roughly 19 MB per 1,024-token request checked in about 17 seconds on CPUs.
  • The code, Lean proofs and documentation are released under Apache 2.0; the authors describe it as a research prototype with clear limits.

Anthropic published FlashProve on November 2, an open-source research system for what it calls provable inference: a way for anyone to verify that a language model's answer was actually generated by a particular model, rather than a cheaper substitute or a tampered version. The work was carried out by Anthropic researchers with cryptographers from EPFL, MIT and the companies StarkWare and Succinct.

How it works

A provider first publishes a short cryptographic commitment, a kind of fingerprint, of its model weights. This offline step took about 39 minutes per model and one commitment covers roughly 16 million requests. For each request, the prover then produces a zero-knowledge succinct argument (zkSNARK) showing that those committed weights, given the prompt, yield the returned tokens. The verifier learns nothing about the weights or intermediate values, nor which experts of the mixture-of-experts model were used; the architecture itself is not hidden.

Anthropic tested the system on Meta's Llama 4 Maverick, a 400-billion-parameter mixture-of-experts model, using a public 4-bit conversion on a single H100 GPU with 24 CPU cores. It reports proving throughput of about 110 tokens per second, at roughly 66 to 95 times the GPU time of serving the same requests with vLLM. Each 1,024-token request yields a proof of about 19 MB, which can be checked in around 17 seconds on 24 CPU threads, without a GPU. The authors say an earlier proof of the same model, VerInf, needed over 14 hours for 1,000 tokens.

The protocol's completeness, soundness and zero-knowledge properties were formally stated and proved in the Lean proof assistant. Code, proofs and documentation are under the Apache 2.0 license.

Limits and possible uses

The authors are explicit about the caveats. The fast C++ verifier has no formal guarantee, although it matched the slower Lean verifier in all tests. Proofs cover an exact integer version of the model with greedy decoding, so sampled outputs are not covered; context is capped at 1,024 tokens; proving happens in batches after the fact; and side channels such as timing are out of scope. The results have not been independently reproduced.

Anthropic suggests such proofs could help users confirm they are getting the model they pay for, give auditors and regulators a way to check providers' claims, and support verification that compute is used only for approved models. It presents provable inference as one tool among others, alongside trusted hardware.