Anthropic released FlashProve on November 2, 2026, an open-source prototype for provable inference: a way for a user to check that a model response came from the specific weights a provider committed to, rather than from a cheaper model substituted by a routing service or from a token stream altered by an attacker. Judging from output alone cannot settle that question, Anthropic argues, even when the output looks good. The release includes executable code, a technical report, a protocol specification and machine-checked proofs in the Lean proof assistant, all under the Apache 2.0 license. Anthropic describes the post as intermediate progress, not a completed research agenda, and the repository is marked as a research artifact that is not maintained and does not accept contributions.[1][2]
The system works in two phases. Offline, the provider publishes a cryptographic commitment to one exact set of weights: a short fingerprint that pins down the weights while revealing nothing about them. The commitment takes about 39 minutes to compute for the model tested, is about 6.5 MB for a verifier to download, and covers roughly 16 million requests before the provider must commit again. Online, after inference has finished, the provider produces a proof file for a batch of completed requests, attesting to one statement: the committed model produces these output tokens on this prompt. Anyone holding the commitment, the prompt and the reply can check the proof on an ordinary CPU, without the weights and without the provider's hardware.[1]
Four properties carry the claim. Completeness: an honest provider's proofs are accepted. Soundness: a proof of a false statement cannot be forged short of breaking widely believed cryptographic assumptions; the repository states that a cheating provider is caught except with probability about q/2^124 + 2^-101 after q hash queries. Zero knowledge: the proof reveals nothing about the weights, the intermediate values, or which experts ran at each layer, although the model architecture itself is not hidden. Succinctness: the attested computation is a run of a 400B-parameter model on an H100, yet the proof is about 19 MB and checks in seconds. Underneath is a zkSNARK of the kind deployed in blockchain layer-2 networks, built by compiling an interactive oracle proof with hash functions, which Anthropic notes also offers post-quantum security.[1][2]
The evaluation uses Llama 4 Maverick, a 400B-parameter mixture-of-experts model with about 17B parameters active per token, in its public 4-bit weights. The prover runs on a single H100 with 24 CPU cores and about 290 GB of host memory, streaming weights in layer segments so one 80 GB GPU suffices. Each request is a window of 1,024 tokens, and each proof checks one token. Proving a batch of 24 requests takes about 223 seconds, roughly 110 tokens per second, and each proof is 18.78 MB. Verification takes 17 seconds on 24 CPU threads, or 21 seconds on a single thread. Against vLLM running the FP8 release of the same model on eight H100s, proving costs about 72 times the GPU time per batch, rising to about 94 times at the highest load tested. Two engineering choices explain much of the speed: the prover's work is proportional to the experts that actually ran, not to all 400B parameters, and requests are proved in batches in a single parallel pass, opening the weight commitment once per batch.[1]
The comparison that matters is with earlier proofs of the same model. VerInf, the only prior system Anthropic knows of that proved Llama 4 Maverick, reported about 0.02 tokens per second, 14.3 hours for 1,000 tokens and a 93.6 GB proof that took almost a day to verify. FlashProve's 110 tokens per second is roughly three orders of magnitude faster, with proofs small enough to check in seconds. Anthropic is careful to note that a commercial system, Attestable, reports 53–77 tokens per second proving a dense 31B model on one H100, but has not released an open-source library.[1]
Proving is post-hoc, not in-line, and Anthropic names the costs of that choice: the provider recomputes the finished text, guarantees about traffic arrive with a delay, and floating-point non-determinism complicates exact matching. The stated limitations are narrow conditions. The proof covers an exact integer version of the published weights under greedy decoding; a reply from a floating-point implementation, or from sampled decoding, can depart from the proved computation at some position. Contexts are limited to 1,024 tokens, far below production chat windows. The construction assumes a mixture-of-experts architecture and does not hide it. Side channels, such as the time taken to produce a proof, are out of scope. And the proof says nothing about whether the model's answer is correct, safe or unbiased; it attests to which weights produced the tokens, not to the quality of the tokens.[1]
The formal verification is unusually prominent, and so are its limits. Anthropic states completeness, soundness and zero knowledge in Lean, in the random oracle model, so the protocol's top-level claims are machine-checkable. It then identifies two remaining trust gaps. First, the formal statements must be audited by hand to confirm they express the intended guarantees; an interactive visualizer is provided to help. Second, the executable code must match the formally defined protocol. For soundness only the verifier matters, and here the split is explicit: the repository ships a Lean verifier that is proved to accept only what the soundness theorem accepts, but it is slow; the C++ verifier recommended for everyday use carries no formal guarantee, though Anthropic says it agreed with the Lean verifier on every proof in its tests. For zero knowledge there is no Lean prover at all, because proving is too expensive to formalize that way; that side rests on audits of the code. The release notes likewise state that Anthropic does not guarantee the Lean protocol, the paper and the fast code all match each other.[1][2]
Anthropic positions the approach against trusted hardware rather than above it. Prior work on provable inference often uses trusted execution environments, whose guarantees rest on the manufacturer producing tamper-resistant hardware. FlashProve is software-only: its security rests on computational hardness assumptions, and an adversary who has compromised the environment, including the hardware or operating system, still cannot produce an invalid proof without solving an infeasible problem. Anthropic calls the two approaches complementary, with different guarantees and tradeoffs. It also notes that the work pursues an objective in its Frontier Safety Roadmap, a prototype for signing inference traffic by September 30, 2026, which Anthropic says it met through a separate, related project that signs traffic and recomputes inference on a trusted server; FlashProve pursues the same goal by a different method.[1]
[1]: Anthropic, "Progress on provable inference for large language models," 2 November 2026. https://www.anthropic.com/research/provable-inference [2]: anthropics/FlashProve, repository README, version 0.16.0. https://github.com/anthropics/FlashProve
Sources
Check or correct this page
Verification record
The digest below shows whether the text you are reading matches the published source. It does not show that the reporting is correct. The build computes it from this page's Markdown source and lists it in the site manifest.
0d073af9f2efb7089d4dfb794d69844862567e84629feadec650be0011df22b2
