Anthropic releases prototype for proving which AI model produced an answer

Checking which AI model answered a request need not mean seeing its secret weights or running it again. On November 2, Anthropic released FlashProve, an open-source research prototype that supplies cryptographic evidence of that computation. Its demonstration offers a way to verify model identity—but at a substantial extra computing cost.

The problem is narrower than whether an answer sounds convincing. A customer using a third-party service may want to know whether the model they paid for actually ran. Independent evaluators likewise need assurance that the model they tested is the one being served. Anthropic presents FlashProve as a tool for those checks, not as a measure of answer quality.

A commitment first, a proof afterward

FlashProve separates setup from individual requests. First, the provider commits to the model’s weights—the numerical values that determine its behavior—and publishes a short cryptographic digest. It then produces proofs that the computation used those committed weights on the client’s input. The digest gives the client a fixed reference without requiring storage of the model itself.

The proof is “zero-knowledge”: it hides the weights and intermediate computation steps. It is also “succinct,” meaning checking the proof requires far less work than repeating the computation. Those properties let a provider keep its weights private while giving a client evidence beyond the generated text. Hiding the model’s architecture is not a goal of this system.

Cheap to check does not mean cheap to produce

The demonstration uses Llama 4 Maverick, a 400-billion-parameter mixture-of-experts model that uses about 17 billion parameters per token. Anthropic’s prover ran on a server with one H100 GPU and 24 CPU cores; verification ran on a CPU. This is a test on that model and configuration, not a benchmark of Claude inference.

Generating proofs consumed roughly 70–95 times the GPU time needed to process equivalent prompts with vLLM, an open-source model-serving library, Anthropic says. That distinction separates the client’s benefit from the provider’s burden: checking can be much cheaper than rerunning a model even while producing the evidence adds considerable work.

The supported computation is restricted, too. The reported proof covers an integer-arithmetic model using greedy decoding, which selects the highest-scoring next token, and contexts of up to 1,024 tokens. The authors describe the release as an early demonstration and say they left possible optimizations out to release it sooner.

The mathematics and the executable have different guarantees

Anthropic says Claude helped develop and optimize the system. To make its security claims auditable, the team supplied top-level mathematical statements and proofs in Lean, a language for machine-checked mathematics. The release includes:

• A technical report and protocol description explaining the construction.
• Executable code with a prover, a fast C++ verifier and a provably correct Lean verifier.
• Lean proofs and an interactive theorem visualizer for auditing. The code, proofs and documentation carry an Apache 2.0 license.

That formal work does not cover every implementation boundary. Anthropic explicitly says it has not formally guaranteed that the fast executable code matches the Lean implementation and paper. The cryptographic analysis also relies on treating BLAKE2’s compression function as an ideal random function. The technical report notes that proofs under this idealized assumption do not themselves formally guarantee security with a concrete hash function.