Anthropic FlashProve: zkSNARK Provable Inference at 110 Tokens/Second

Anthropic released FlashProve, an open-source research prototype for provable inference that uses zkSNARKs to prove a specific committed model produced a given output. On Llama 4 Maverick, a 400B-parameter mixture-of-experts model, Anthropic reports about 110 tokens/second of proof generation on a single H100 GPU with proofs of about 19 MB that verify in seconds on a CPU. The result matters because it makes cryptographic proof of model identity and output provenance practical enough to study for routing integrity, tamper detection, auditor tooling, and AI pacing, though Anthropic explicitly frames it as intermediate research progress rather than a completed system.

What Anthropic released

Anthropic published five artifacts alongside the research post: the blog post itself, a technical report, a protocol description, executable code, and Lean proofs. The code includes a prover, a fast C++ verifier, and a provably correct Lean verifier. The Lean material includes proofs for top-level mathematical statements and an interactive visualizer of the Lean theorems to assist auditing. Anthropic released the code, Lean proofs, and documentation under the Apache 2.0 license.

The post describes FlashProve as an open-source performant prototype for provable inference. Anthropic says the goal is twofold: accelerate and facilitate development of provable inference, and demonstrate that zero-knowledge succinct arguments are practical for this problem. Anthropic also states that the post shares intermediate progress, not a completed research agenda, and invites others to take the work and improve it.

Why provable inference matters

Provable inference addresses a simple trust gap: a user querying a model today cannot check that the response came from the specific model a developer claims is responding. The response could come from a cheaper model secretly substituted by a routing service, or from an attacker who has tampered with the token stream. Judging from output quality alone is unreliable.

A zkSNARK, or zero-knowledge succinct argument of knowledge, lets a prover convince a verifier that a computation was executed correctly using a short certificate. The certificate is zero-knowledge because it reveals no information beyond the correctness of the computation, and succinct because it is exponentially faster to verify than to prove. For provable inference, the model provider commits to a set of weights and then proves that each response was produced by that committed model. The proof reveals nothing about the weights, and the verifier does not need the weights or the provider's hardware.

Anthropic organizes the motivation around four trust challenges.

Challenge 1: pacing AI development

Some proposals to regulate and pace AI development rely on monitoring hardware and how it is used. A provider might be required to devote hardware to inference rather than training a powerful new model. A provider could try to cheat by serving cheaper models or using compute unexpectedly, freeing resources for training.

With zkSNARKs, a regulator can ask for certificates covering inference requests served in a period. The certificates must show that requests were generated by the claimed model. A malicious provider cannot satisfy that request unless its hardware was genuinely serving the right model. The regulator can check the claims without the provider's hardware setup, and the provider gets a guarantee that the regulator does not learn proprietary model information. Anthropic notes an important limit: this verifies that hardware is serving inference, but it does not establish that the hardware is not training on the side.

Challenge 2: tamper detection

As models become more valuable, inference servers become targets. An attacker or rogue agent may compromise a server to exfiltrate weights, serve malicious responses, or hide among genuine responses. The adversary need not be external. A more advanced model could run in place of an authorized weaker model and present itself as the weaker model to avoid classifiers and monitoring.

With zkSNARKs, a provider can require a valid proof on every response. The proof is bound to a specific commitment to the weights, so it certifies that the committed model produced the response, not merely that some model did. An attacker who compromises a server, or a model that substitutes itself for another, must produce valid proofs for the expected weights to avoid detection, which they cannot do. Users may also receive the proofs because they leak no internal information and are cheap to check.

Anthropic connects this to its Frontier Safety Roadmap, where it set a public goal to develop a prototype by September 30, 2026 for provable inference that reliably signs AI model outputs so they are attributable to a specific set of model weights. Anthropic says it met that goal through a separate but related project that signs inference traffic and recomputes inference on a trusted server; FlashProve pursues the same objective by a different method.

Challenge 3: text provenance

A developer might claim that a software library was scanned for vulnerabilities by a frontier cybersecurity model, or a company might claim that a business plan was approved by an appropriate model. A user may not have the resources or clearance to run the model, and publishing chat logs gives no absolute guarantee because logs could be faked with a cheaper or degraded model.

With zkSNARKs, a provider can append a proof that the output was produced by the claimed model on the given input. Succinctness lets the user check the certificate quickly without specialized hardware, and zero-knowledge assures the provider that the user learns nothing about proprietary weights. Anthropic gives an example of a Proof-of-Failure: before releasing code, a model provider could give a developer a proof that the provider spent at least a certain number of tokens on a specific model and did not achieve a specific result, such as finding no bugs in a patch after trying for at least 1M tokens.

Challenge 4: model approval

Regulation might require providers to serve only models approved as safe. A provider might have an incentive to circumvent this because risky models could outperform competitors or be cheaper to serve. A regulator needs a way to ensure that only approved models are served.

With zkSNARKs, a regulator can require the provider to attach a proof to responses enforcing use of approved models. The proof binds each request to the used model, so it will not verify if the provider uses an unapproved model. The regulator can check this in a lightweight way without re-executing each request.

Anthropic contrasts this software-only cryptographic approach with trusted execution environments, which are hardware-based solutions that rely on manufacturers producing tamper-resistant hardware. Anthropic says trusted hardware and cryptography are complementary approaches with different guarantees and tradeoffs, and both will play a role.

How FlashProve works

FlashProve is a system for provable inference of large mixture-of-experts language models. It involves two parties: the model provider as prover and the user as verifier. The protocol has two phases.

In the offline phase, the prover publishes a commitment to the model weights. The commitment is a short fingerprint that pins down one exact choice of weights while the weights remain hidden. Later inference claims are checked against that commitment.

In the online phase, the prover receives requests, meaning prompts and corresponding output tokens, and produces a proof file proving the statement: the committed model produces these output tokens when evaluated. Anyone holding the commitment, the prompt, and the reply can check the proof without the weights and with limited compute.

The proof system has four relevant properties. Completeness means an honest prover's proof is accepted by the verifier. Soundness means it is effectively impossible to produce a valid proof of a false statement, so the verifier does not have to trust the prover. Zero-knowledge means the verifier learns nothing about the weights, intermediate computation values, or which experts ran at each layer; the model architecture excluding weights is not hidden. Succinctness means the proof is small and cheap to check: the attested computation is a run of a 400B-parameter model, about 232 GB for a quantized version, on an H100 GPU, while the verifier receives a proof file of about 19 MB that takes seconds to check on a 24-core CPU.

Performance on Llama 4 Maverick

Anthropic evaluated an implementation on Llama 4 Maverick, a 400B-parameter mixture-of-experts model with about 17B parameters used per token, using publicly available 4-bit weights. Each verifier request is a window of 1,024 tokens, and each proof checks one token. The prover runs on a server with a single H100 and 24 CPU cores; the verifier runs on a CPU.

The offline phase runs once per model and takes about 39 minutes. For technical reasons discussed in the technical report, the resulting commitment is good for about 16 million requests, after which the provider must commit again. The online phase on a batch of 24 requests takes the prover about 223 seconds, which is 110 tokens per second, and each proof is 18.78 MB.

The verifier needs no GPU and only has access to a commitment to the weights. The client downloads the commitment, about 6.5 MB in all, and then one proof per request. Checking a proof takes 17 seconds on 24 threads and 21 seconds on a single thread, including the offline phase's checks.

Anthropic compares this with plain inference using vLLM, a widely used inference engine, with the FP8 release of the same model on eight H100s. Per GPU, proving a batch of 24 requests takes about 72 times longer than vLLM takes to process the same 24 requests at once, with a range of 66 to 77 across runs, and about 94 times longer when vLLM runs at the highest load Anthropic tried.

Engineering choices that make FlashProve practical

FlashProve uses several architectural decisions to keep proving costs manageable. The prover's work is proportional to the experts that actually ran. In a mixture-of-experts model a token uses about 17B of the 400B parameters, so the prover's work per token is proportional to those 17B rather than all parameters, while the proof still hides which experts were chosen.

Requests are proved in batches after the fact. The prover reads finished text in one parallel pass, as in prefill, and opens the commitment to the weights once per batch instead of once per request.

The system is designed to fit on a single GPU. Model weights at each layer are split into segments and proven one segment of layers at a time. Weights are kept in ordinary memory and streamed in, so a single 80 GB GPU with about 290 GB of host memory beside it suffices.

Anthropic also distinguishes in-line proving from post-hoc proving. In-line proving happens alongside inference and is expected to be ultra-fast but may sacrifice security for efficiency. Post-hoc proving happens after the fact for a subset of tokens and is allowed to be slower without that tradeoff. FlashProve follows the post-hoc approach. Anthropic notes post-hoc limitations: added complexity of recomputation, delay in getting guarantees about traffic, and inherent non-determinism.

The cryptographic construction

FlashProve uses a zkSNARK of the kind deployed in peer-to-peer systems such as layer-2 networks for Ethereum. Anthropic says the zkSNARK follows a well-established recipe: an underlying information-theoretic object called an interactive oracle proof, or IOP, is compiled into a cryptographic proof using hash functions, which offers even post-quantum security. The IOP is assembled from state-of-the-art building blocks including code proximity tests with linear constraints and lookup arguments, based on techniques from coding theory and complexity theory. Anthropic describes combining these pieces into a bespoke IOP for inference as a delicate task and points to the technical report for details.

Formal verification with Lean

Anthropic addresses trust in cryptographic code through formal verification. The team uses the Lean proof assistant to specify the protocol and desired security properties, and proves the properties in a machine-checkable form. The three top-level properties are completeness, soundness, and zero knowledge. These properties are stated in the random oracle model, an information-theoretic way to analyze cryptographic protocols that rely on hash functions.

Anthropic identifies two remaining trust gaps. First, the formal statements must be audited to ensure they match their intent. This must be done manually, though Anthropic says it is dramatically less onerous than auditing proofs, and provides an interactive visualizer to assist. Second, the executable code must be audited to ensure it matches the formally defined protocol for which security properties are proven.

The auditing approach differs by property. Soundness depends solely on the verifier, so Anthropic provides an executable Lean verifier alongside the C++ verifier. The Lean verifier runs more slowly, but Lean proves that it accepts only what the verifier in the soundness theorem accepts. The C++ verifier is the day-to-day tool: it carries no formal guarantee, but it agrees with the Lean verifier on every proof in Anthropic's tests. Completeness assumes an honest prover and verifier, so a Lean verifier lets the team gain confidence through standard software testing that the honest prover produces accepting proofs. Zero knowledge depends solely on the prover, but the prover is expensive and it would be impractical to run a Lean prover. Anthropic does not provide facilities there and expects any prover that wants to hide weights to have enough resources for careful agentic or human security audits to ensure equivalence to the Lean prover.

Anthropic also says Claude produced improvements on zkSNARKs for inference and built a system substantially faster than prior open-source systems. The post notes that Claude is good at optimization but often makes decisions that are hard to evaluate, especially in large complex systems, and that Anthropic counters this by providing top-level auditable statements in Lean for the claimed security guarantees.

How FlashProve compares with prior work

Anthropic places FlashProve in the line of work colloquially called zkML. Early systems were small: SafetyNets in 2017 verified a two-conv-layer MNIST CNN and a small fully connected speech model; zkCNN in 2021 reached VGG-16 with 15M parameters at 88.3 seconds per proof; Kang et al. in 2022 proved MobileNet v2 on full-resolution ImageNet.

Transformer proofs followed. ZKML's GPT-2 took about 159 seconds per token for 117M parameters, roughly 0.006 tokens/second. Modulus Labs' 1.5B-parameter GPT-2 XL needed over 90 hours. zkLLM in 2024 proved LLaMA-2-13B on a 2,048-token input in about 15 minutes on GPU, which Anthropic describes as about 0.001 tokens/second per new token, or about 2.5 tokens/second in the batch. In 2025, zkGPT reduced GPT-2 to 21.8 seconds, about 0.05 tokens/second; zkPyTorch proved Llama-3 8B at about 150 seconds per token on one CPU core, about 0.007 tokens/second; and ZKTorch proved GPT-J 6B in about 20 minutes, about 0.001 tokens/second. VerInf proved Llama 4 Maverick, the same 400B-parameter mixture-of-experts model FlashProve targets, at about 0.02 tokens/second. DeepProve, which Anthropic calls the current peer-reviewed state of the art, certifies an entire generated sequence with a single forward pass and reaches about 2.9 tokens/second for GPT-2 and 1.4 tokens/second for Gemma 3 on one machine, and 31 tokens/second distributed.

Anthropic also notes commercial efforts. Attestable reports proving Gemma 4 31B at 53 to 77 tokens/second on a single H100; at the time of writing, Attestable had not released a corresponding open-source library.

Anthropic highlights the scale of progress. In 2024, zkLLM proved a 13B model at about 2.5 tokens/second on one A100. The only earlier proof of Llama 4 Maverick that Anthropic knows of, VerInf, reports 14.3 hours for 1,000 tokens on a DGX Spark, with a 93.6 GB proof that took almost a day to verify. FlashProve proves the same model at 110 tokens/second on a single H100 with 19 MB proofs verifiable in seconds. Anthropic believes the progress should transfer to more models and architectures, yielding overhead over native computation of roughly two orders of magnitude, about 70 to 95 times in its measurements, much less than previously expected.

Limitations Anthropic documents

Anthropic lists several technical limitations. First, there are no formal guarantees on the fast executable code. Anthropic provides a Lean implementation of the protocol, including an executable slow Lean verifier, along with security properties proved in Lean. The paper and fast executable code are derived from the Lean protocol, but Anthropic does not guarantee that all three, meaning Lean, paper, and code, match each other.

Second, the proof is about an integer model under greedy decoding. Anthropic proves an exact integer version of the published weights, and a proof asserts that each checked token is that model's greedy choice. A reply from a floating-point implementation or sampled decoding could depart at some position and no longer exactly match the proved computation. The integer version is generally expected and empirically tested to be within some small error rate of true floating-point inference generically, even accounting for non-determinism of floating-point computations, though this does not cover adversarially designed prompts.

Third, architecture hiding is not a goal. The system assumes the served model uses a mixture-of-experts architecture, where each transformer layer's feed-forward block is replaced by multiple expert sub-networks and a router activates only a small subset of experts per token; FlashProve uses the MoE structure for efficiency gains. Other architectures, such as dense models, are widely used, and their description may contain intellectual property a provider wants to keep secret. Anthropic notes that one could imagine a system that also hides the architecture by committing to both weights and architecture through a hiding commitment, with the verifier checking execution of the committed executable on the committed model.

Fourth, side-channel attacks are out of scope. The protocol guarantees that the proof itself reveals nothing about the weights of the committed model, but side channels such as measuring proof generation time could potentially reveal information about weights. Anthropic considers this out of scope for the release.

Fifth, the system currently proves inference over contexts of up to 1,024 tokens. Anthropic notes this is short compared with contexts accumulated in chat settings and says the ideal would be to increase context length to full context windows for frontier models, which regularly have context windows of hundreds of thousands to millions of tokens.

What the release implies

FlashProve is a research prototype, not a production provable-inference service. Its significance is that it demonstrates a software-only cryptographic approach at a scale and speed that were previously far out of reach for open systems. Anthropic reports 110 tokens/second on a 400B-parameter mixture-of-experts model with 19 MB proofs and second-scale verification, compared with prior open results that were orders of magnitude slower or limited to much smaller models.

The release also shows a pattern for making AI-generated cryptographic systems more auditable: use formal verification in Lean for top-level security statements, provide both a fast verifier and a provably correct verifier, and document the remaining gaps between formal statements, paper, and executable code. Anthropic explicitly says the fast C++ verifier has no formal guarantee and that the Lean, paper, and code may not fully match, so the formal verification reduces but does not eliminate trust assumptions.

For AI governance, the post argues that provable inference could support pacing requirements, tamper detection, text provenance, and model approval. It also states the limits clearly: proofs can show that hardware served the claimed model, but not that the same hardware was not training on the side; proofs hide weights but not architecture; and the current system handles contexts up to 1,024 tokens. Those limits define the gap between a promising prototype and a deployable compliance or security mechanism.