# Provable inference with FlashProve: Llama 4 Maverick proofs at 70-95x vLLM GPU time

> Anthropic released FlashProve, a zkSNARK system that proves a response came from committed model weights without revealing them. On one H100 it costs about 70-95x the GPU time of serving with vLLM.

- Published: 2026-11-04
- By: Samir Sengupta (https://www.samcodeman.com/about)
- Canonical: https://www.samcodeman.com/writing/flashprove-provable-inference-llama-4-maverick-70-95x
- How this was made: Drafted with Claude, Anthropic's model from 1 cited source, then checked against it in a second editing pass. Editorial policy: https://www.samcodeman.com/editorial-policy

## The short version

- A FlashProve proof binds each response to a commitment to specific weights while hiding those weights. Per Anthropic, a compromised server or a substituted model cannot produce valid proofs for the expected weights.
- The serving overhead is large. For a 400B mixture-of-experts model, one H100 proves about 110 tokens/second, roughly 70-95x the GPU time of running it on vLLM, plus about 19 MB of proof per 1,024-token request.
- Security rests on computational hardness assumptions rather than tamper-resistant hardware. The top-level guarantees are stated in Lean so they can be audited.
- The release is a research prototype demonstrated on Llama 4 Maverick. The post does not say that Claude responses ship with proofs today.

Anthropic has released FlashProve, an open-source prototype for provable inference. A model provider commits to a set of weights, then attaches a zkSNARK to each response proving it was produced by the committed model, and the proof reveals nothing about the weights. On Llama 4 Maverick (400B-parameter mixture of experts, 4-bit quantized weights), a single H100 generates proofs at around 110 tokens/second. Each 1,024-token request produces a proof of about 19 MB, and proving takes roughly 70-95x the GPU time of running the model on vLLM.

The problem Anthropic names is that a user querying a model cannot currently check which model answered. A routing service might swap in a different model for cost reasons, or an attacker might tamper with the token stream, and judging from the output alone is unreliable. The authors are Roy Rinberg and Alex Allain (Anthropic), Alessandro Chiesa (EPFL, StarkWare), Miranda Christ (MIT, RESI), Rahul Dalal (Anthropic STEM Fellows Program, Succinct), Giacomo Fenzi (EPFL), Ben Mayer (Anthropic Fellows Program, MIT) and Guy Weissenberg (EPFL). Anthropic describes the post as intermediate progress, not a completed research agenda, shared so that others can take the work and improve it.

## What a FlashProve proof binds to

FlashProve uses a zkSNARK, a zero-knowledge succinct argument of knowledge. The provider commits to a model, and each proof is bound to that commitment, so it certifies that the committed model produced the response rather than some model. Zero knowledge means the proof reveals nothing beyond the computation's correctness. Succinctness means, in Anthropic's words, that it is exponentially faster to verify than the proved computation. Anthropic's illustrative target is a proof of a few megabytes, checkable ideally in seconds on a CPU, while the measured Maverick proof is about 19 MB per 1,024-token request.

> The commitment to the model, and subsequent inference proofs, hide the weights of the model; hiding the architecture of the model is not a goal of this system.
>
> - Anthropic, Progress on provable inference for large language models

The proof does not certify everything. One Hacker News commenter pointed out that it tells you nothing about whether your data was exfiltrated and no useful property of the answer itself. The proof covers provenance only. Another commenter noted that proving output correct against a source of truth is a separate problem.

## Serving cost: 110 tokens/second per H100

For Llama 4 Maverick, a 400B-parameter mixture of experts, proving runs at about 110 tokens/second on one H100, using 4-bit quantized weights and integer arithmetic in prefill. That is about 70-95x the GPU time vLLM takes to process prompts of the same length. Each 1,024-token request also produces about 19 MB of proof that has to be stored or sent to the verifier. Anthropic says prior open-source systems are orders of magnitude slower and discusses them in section 6 of the post, which the available excerpt does not include.

- Prover: around 110 tokens/second on a single H100 for Llama 4 Maverick, 4-bit.
- Proof size: about 19 MB per 1,024-token request.
- Relative cost: about 70-95x the GPU time of vLLM processing prompts of the same length.
- Verifier: two implementations ship, a fast verifier in C++ and a provably correct verifier in Lean. The excerpt gives no measured verification time.

At these figures, proving every response would need far more GPU capacity than serving it. Anthropic's tamper-detection scenario has a provider require a proof on every response. Its pacing scenario has a regulator request proofs covering the requests served in a given period. The post does not discuss sampling strategies or what fraction of traffic would need proofs in practice.

## Does provable inference catch silent quantization?

One commenter on Hacker News asked whether this would catch hosts that serve named models quantized without saying so. The commitment is to a specific set of weights, and the Maverick demo proves a specific 4-bit quantization. That suggests a host committed to one quantization could not produce valid proofs for responses from another, though the excerpt does not address quantization swaps directly. Another commenter, citing the repository docs, said open-weight models are supported this way. In that account, the provider commits using the public weights and publishes the seed, so anyone can recompute the commitment from the Hugging Face files and check the exact checkpoint and quantization.

Commenters quoting the project documentation said the proof covers an exact integer version of the published weights and asserts that each checked token is that model's greedy choice. On that reading, sampled decoding and floating-point serving are not directly covered. They also quoted that the integer version is empirically tested to be within a small error rate of floating-point inference, but this does not cover adversarially designed prompts. One commenter added that support is currently limited to greedy decoding and short contexts. The blog excerpt does not state these limits, so treat them as claims to check against the repository.

## Trust assumptions: hardness, not hardware

Prior work on provable inference often focuses on trusted execution environments, which rely on the manufacturer producing tamper-resistant hardware. FlashProve is software-only, and its security rests on the hardness of computational problems. Anthropic says that even with compromised hardware or operating system, an adversary cannot produce an invalid proof without breaking a computationally infeasible problem. Anthropic calls the two approaches complementary, with different guarantees and tradeoffs. One commenter suggested TEEs may be a cheaper route given the 70-95x overhead.

A second trust question is whether the implementation is right. Anthropic credits Claude with the zkSNARK improvements behind FlashProve, and the protocol specification is Claude-written. Anthropic acknowledges that Claude often makes decisions that are hard to evaluate in large complex systems. Its countermeasure is to state the top-level security guarantees in Lean, with an interactive visualizer of the theorems for auditors. The excerpt does not say how the fast C++ verifier is tied to the Lean verifier.

## Where Anthropic expects the proofs to be used

Pacing: a regulator checks that hardware was serving the claimed model. Anthropic notes this does not establish that the hardware is not also training on the side. Tamper detection: a provider requires a valid proof from every server, so a compromised server, or a more advanced model running in place of the authorized one and presenting itself as the weaker model, cannot produce valid proofs. Text provenance includes a proposed Proof-of-Failure, for example showing that a model spent at least 1M tokens on a patch without finding bugs. Model approval: a regulator requires proofs so that only approved models are served.

In its Frontier Safety Roadmap, Anthropic set a goal of a provable inference prototype by September 30, 2026, and says it met that goal through a separate project. That project signs inference traffic and recomputes inference on a trusted server, while FlashProve pursues the same objective by a different method. The post does not say that Claude API responses carry FlashProve proofs, and the demo model is Llama 4 Maverick. One commenter linked a Fortune report and argued that it showed Anthropic itself silently limiting responses to some requests. Proofs only address that kind of concern if a provider attaches them to the responses customers receive.

## What ships under Apache 2.0

Anthropic released five artifacts. The code, Lean proofs and documentation are under the Apache 2.0 license.

1. The blog post outlining the system and its potential applications.
2. A technical report with the system details.
3. A Claude-written protocol specification.
4. Executable code: a prover, a fast C++ verifier and a provably correct Lean verifier.
5. Lean proofs of the top-level mathematical statements, with an interactive visualizer.

For teams that route traffic through third-party providers, the near-term use, per commenters' reading of the repository docs, is checking that an open-weight checkpoint and quantization match what a host claims, at a steep GPU cost. Sampled decoding, long contexts and proofs on closed frontier models are not demonstrated in the released material.

## Questions this raises

### How expensive is provable inference with FlashProve?

On Llama 4 Maverick with 4-bit weights, one H100 proves about 110 tokens/second, roughly 70-95x the GPU time of serving with vLLM. Each 1,024-token request also yields about 19 MB of proof to store or send.

### Does FlashProve catch a host serving a silently quantized model?

The proof is bound to a commitment to specific weights, and the Maverick demo proves a specific 4-bit quantization, which suggests a different quantization could not produce valid proofs. The excerpt does not address quantization swaps directly, though commenters say open-weight commitments can be recomputed from the public files.

### Does FlashProve rely on trusted hardware like TEEs?

No. FlashProve is software-only and its security rests on the hardness of computational problems, so compromised hardware or an OS cannot forge a proof. Anthropic calls it complementary to trusted execution environments.

## Key facts

- FlashProve proves Llama 4 Maverick (400B MoE, 4-bit weights) at about 110 tokens/second on a single H100.
- Each 1,024-token request produces a proof of about 19 MB.
- Proving costs roughly 70-95x the GPU time vLLM takes to process prompts of the same length.
- Two verifiers ship: a fast one in C++ and a provably correct one in Lean; no verification time is given.
- Commenters quoting the docs say support is limited to greedy decoding and short contexts on an integer version of the weights.

## Sources

1. [Progress on provable inference for large language models](https://www.anthropic.com/research/provable-inference) - anthropic.com

Discussion read (practitioners' reactions, not a source): https://news.ycombinator.com/item?id=50368626