Anthropic's FlashProve cryptographically proves which AI model answered you

What this is about

On November 2, 2026, Anthropic released FlashProve, an open-source prototype for "provable inference." The system is meant to show that a response was really generated by a specific, pre-committed model. Users should be able to check this without knowing the model's weights and without re-running the model themselves.

The problem: when you send a request to an AI model today, you can't be sure which model answers. A routing service could quietly swap in a cheaper model to save money. An attacker could tamper with the token stream. According to Anthropic, you also can't reliably tell from the quality of the answer. Anthropic stresses that this is an interim research result, not a finished product.

Five artifacts were published: a blog post, a technical report, a protocol specification (written by Claude), runnable code with one prover and two verifiers (a fast one in C++ and a formally verified one in Lean), and Lean proofs of the key claims, plus an interactive visualizer. Everything is available under Apache 2.0 in the GitHub repository anthropics/FlashProve. Besides Anthropic staff (Roy Rinberg, Alex Allain), researchers from EPFL, MIT and people associated with StarkWare and Succinct took part.

How FlashProve works

The foundation is a zkSNARK ("zero-knowledge succinct argument of knowledge"). This is a cryptographic proof that lets one party (the prover) convince another (the verifier) that a computation ran correctly. The proof reveals nothing about secret inputs (zero-knowledge) and is much faster to check than the computation itself (succinct). The same technique is used in the blockchain world, for example in layer-2 networks like Starknet.

The process has two phases:

• Offline phase: The provider publishes a "commitment," a kind of short fingerprint that pins down exactly one set of weights while the weights stay secret. It takes about 39 minutes per model. The commitment is around 6.5 MB and is good for roughly 16 million requests.
• Online phase: For a given prompt and response, the provider generates a proof file for the statement "the committed model produces these output tokens." Anyone with the commitment, prompt and response can verify it.

Four properties are meant to hold. Honest proofs are accepted (completeness). False proofs can't practically be forged without breaking standard cryptographic assumptions (soundness). The verifier learns nothing about the weights, intermediate values, or which experts ran in each layer (zero-knowledge). And the proof is small and cheap to check (succinctness). The model's architecture, by contrast, stays visible. Hiding it is not a goal.

The scheme is hash-based, uses an interactive oracle proof, and, according to Anthropic, even offers post-quantum security. It is a pure software approach. Unlike solutions based on trusted hardware (trusted execution environments), security doesn't depend on a chip vendor but on the hardness of mathematical problems. Anthropic sees the two approaches as complementary.

Numbers and benchmarks

The test model was Llama 4 Maverick, a mixture-of-experts model (only a subset of "expert" subnetworks is used per token) with about 400B parameters, roughly 17B of them active per token, using publicly available 4-bit weights (about 232 GB). The prover ran on a server with one H100 and 24 CPU cores.

The comparison is against vLLM running the FP8 version of the model on eight H100s, measured per GPU. Overall, Anthropic puts the cost at 70 to 95 times the GPU time.

For comparison with earlier work (figures per Anthropic): zkLLM proved a 13B model in 2024 at about 2.5 tokens/s in a batch. The only known earlier work on Maverick, VerInf, needed 14.3 hours for 1,000 tokens on a DGX Spark, with a 93.6 GB proof that took almost a day to verify. A commercial company, Attestable, reports 53–77 tokens/s for Gemma 4 31B on an H100 but hasn't released an open-source library for it.

Three design decisions make this possible. The cost scales with the experts that are actually active (around 17B rather than 400B), without revealing which ones they were. Requests are proven after the fact in batches, and the commitment is opened only once per batch. And the weights are streamed layer by layer from main memory, so an 80 GB GPU plus about 290 GB of host memory is enough.

Applications and trust through Lean

Anthropic names four areas of application:

• Pacing/regulation: Regulators could demand proof that hardware was actually serving inference. That doesn't prove it isn't also being used for training on the side.
• Tamper detection: A compromised server, or a model posing as a weaker one, couldn't produce valid proofs for the expected weights. In its Frontier Safety Roadmap, Anthropic had set itself the goal of building a prototype by September 30, 2026. It says this goal was met through a separate project that signs traffic and recomputes it on a trusted server.
• Provenance of text: For example, a "proof of failure" showing that a model spent at least a million tokens and found no bug in a patch.
• Model approval: Regulators could enforce that only approved models run.

Cryptographic code is error-prone, so Anthropic specifies the protocol and its security properties in the Lean proof assistant (completeness, soundness, zero-knowledge, in the random oracle model). Two gaps remain: the formal statements have to be checked by hand (the visualizer is there for that), and the executable code has to match the protocol. For soundness, only the verifier matters. The Lean verifier is slow but formally tied to the soundness theorem. The fast C++ verifier has no guarantee and agreed with the Lean verifier in all tests. According to unite.ai, the project documents also state that AI systems, under human direction, wrote almost all of the software, the Lean proofs and the documentation, that no independent security review took place, and that tests of weight hiding and attack proofs are limited. The repository is labeled an unmaintained research artifact (version 0.16.0) and doesn't accept contributions.

Limitations

• The proof applies to an exact integer version of the weights under greedy decoding (always the most likely token). Responses from floating-point implementations or sampled outputs may differ. It hasn't been tested against specially crafted prompts.
• The system requires an MoE architecture and relies on it for efficiency. Dense models aren't covered.
• Contexts are capped at 1,024 tokens, far less than is typical in chat scenarios.
• Side-channel attacks, such as measuring proving time, are explicitly out of scope.
• Proving after the fact brings recomputation, delayed guarantees and nondeterminism.
• Code, paper and Lean protocol don't have to match exactly.

What you need to try it

This isn't for home users. According to the source, the prover needs an 80 GB GPU (H100), 24 CPU cores and around 290 GB of RAM, plus the Maverick weights at about 232 GB. Verification, by contrast, runs in seconds on an ordinary multicore CPU without a GPU. It's a research artifact for developers and cryptography enthusiasts, not an everyday tool.

Our take

FlashProve shows that cryptographic proofs for a 400B-class model are becoming practical on a single GPU. The leap over earlier open systems is huge (a factor of 5,000 or more compared with VerInf). Note, though, that the figures come from Anthropic and, according to BigGo, haven't yet been independently reproduced. For everyday use it's still far off: 70 to 95 times the compute and 19 MB per request are better suited to spot checks and audits than to every interaction. Add the narrow greedy-integer assumption, the 1,024-token limit and the lack of independent review. It's interesting for independent evaluators, providers of routing services and regulatory approaches that have so far lacked a verifiable proof of which model ran. That Claude took over large parts of the development is remarkable, but it makes formal verification all the more important. Anthropic gives no timeline and no plans for commercialization.