Anthropic Releases FlashProve for Cryptographic AI Inference Proofs

Anthropic released FlashProve on November 2, 2026: an open-source research prototype that uses cryptographic proofs to show a language-model response came from committed weights without revealing them. The company reported proof generation at 110 tokens per second for Meta’s Llama 4 Maverick.

The work addresses a verification gap in hosted AI. A high-quality answer does not establish which model produced it: a routing service could substitute another system, an evaluator could receive a different model from the one intended for testing, or an attacker could alter the token stream. Checking by rerunning the model is impractical for users when weights are private and the hardware requirements are substantial.

Binding Responses to Hidden Weights

FlashProve uses a zero-knowledge succinct argument of knowledge, or zkSNARK, in a software-only design rather than depending on trusted hardware. During an offline phase, the provider publishes a short commitment that identifies one exact set of weights while keeping them secret. For completed prompt-and-response pairs, the system produces a proof that the output tokens are the committed model’s output. Anyone holding the commitment, prompt and reply can check the proof without access to the weights.

The intended properties are completeness, soundness, zero knowledge and succinctness. An honest proof should be accepted, while certifying a false statement should require breaking widely believed cryptographic assumptions. Checking a proof should reveal neither the weights nor intermediate computation values. The design also conceals which mixture-of-experts subnetworks ran for each token, although the model’s architecture itself remains visible.

The implementation takes advantage of Maverick’s mixture-of-experts structure. Prover work scales with the roughly 17 billion parameters active for a token rather than all 400 billion, while still hiding the expert choices. Segmented weights are streamed from host memory, allowing the prover to fit on one 80 GB GPU with about 290 GB of host memory alongside it.

Anthropic describes possible uses in customer integrity checks, independent evaluations, regulatory tools and enforcement of approved-model requirements. Inference certificates could attest that requests were served by a claimed model, but they would not establish that the same hardware was not also training another model. That distinction limits what such certificates could demonstrate about compliance requirements based on how computing capacity is used.

Proof Performance and Inference Overhead

Anthropic’s evaluation used a publicly available 4-bit conversion of the model. A server with one H100 and 24 CPU cores proved a batch of 24 requests in about 223 seconds, producing an 18.78 MB proof for each request. The offline commitment step took about 39 minutes.

On the verification side, the client downloads an approximately 6.5 MB commitment and checks proofs on a CPU without a GPU. Anthropic measured verification at 17 seconds with 24 threads and 21 seconds with one thread, including the offline phase’s checks.

Those measurements separate a CPU-only checking process from a much heavier proving operation. In Anthropic’s comparison with FP8 inference on eight H100s running vLLM, proving required about 72 times as much per-GPU time for the same batch and about 94 times as much at the highest vLLM load tested. The throughput therefore comes with a substantial cost relative to serving the model without proofs.

Formal Verification and Practical Limits

The FlashProve repository contains a prover, a fast C++ verifier, a slower Lean verifier, Lean proofs of top-level mathematical statements and an interactive theorem visualizer under the Apache 2.0 license. It labels version 0.16.0 as an unmaintained research artifact that is not accepting contributions.

The Lean work addresses completeness, soundness and zero knowledge in the random-oracle model. The formal statements still require manual review to establish that they express their intended guarantees. The Lean verifier is formally connected to the soundness theorem, but the C++ verifier intended for routine use carries no formal guarantee and was instead tested for agreement with the Lean verifier.

The project’s known-limits documentation records that AI systems under human direction wrote nearly all of the software, Lean proofs and documentation and ran the reported tests. There has been no independent security audit, and testing of weight hiding and adversarial proofs remains limited.

The proofs cover an exact integer version of the weights under greedy decoding. Floating-point inference or sampled decoding can depart from the computation being proved, and the generic error testing does not cover adversarially designed prompts. Contexts are limited to 1,024 tokens, while timing and other side-channel attacks fall outside the guarantee. Post-hoc proving also introduces recomputation, delayed assurances and non-determinism compared with proving alongside inference.

For provable inference to become a routine check on served traffic, the remaining work is concentrated in the gaps this release exposes: lowering proving cost, covering less restrictive decoding and longer contexts, and connecting the fast implementation more firmly to the formal protocol.