Anthropic FlashProve: How Provable Inference Works and Where It Falls Short

Anthropic has released FlashProve, an open-source research prototype for checking whether an AI response matches a committed model. The useful idea is that a customer could verify what ran without receiving the model's private weights. The current implementation, however, is much narrower than a verification badge for every Claude response.

What Anthropic released

Anthropic's research announcement, dated November 2, describes work with academic collaborators on provable inference. The release includes a technical report, executable software and formal proofs written in Lean.

This matters when the model itself is part of what someone is buying or evaluating. A convincing response does not tell an evaluator whether the provider used the expected model, and an API's model name alone is still a claim made by that provider.

FlashProve explores a cryptographic way to make that claim checkable. It is research code, rather than a newly available Claude API feature. The repository explicitly says it is not maintained and is not accepting contributions. Its code is Apache 2.0, while the separately downloaded Llama weights retain their own licence.

How FlashProve verifies a model

The provider first creates a commitment, a cryptographic reference to particular weights. Later, it produces a proof about a computation using those weights. A verifier can check that proof without possessing the model or running the same expensive computation.

The intended privacy property is that the proof does not disclose the weights. The architecture is not hidden. FlashProve uses zero-knowledge proof techniques and exploits the sparse computation of mixture-of-experts models, where only part of the network is active for a token.

There is an important setup requirement: the verifier needs a commitment associated with the model they actually trust. Taking an arbitrary commitment from the server being checked would only establish consistency with whatever model that server selected.

For an API marketplace, this suggests a useful division of responsibilities. A lab could establish the model reference, while a separate serving company supplies responses and proofs. Whether that becomes practical depends on the cost and coverage of verification.

What the 110 tokens-per-second result measures

The experiment uses a public 4-bit version of Llama 4 Maverick, a 400-billion-parameter mixture-of-experts model. The performance documentation makes the measurement conditions especially important.

Measurement	Reported setup or result
Proving hardware	One NVIDIA H100 80 GB, with substantial host memory
Context per request	1,024 tokens
Batch size for headline result	24 requests
Steady prefill proving rate	About 111 tokens per second
Batch time	Roughly 221 to 226 seconds
What each timed proof checks	The next token

This is not a text-generation speed benchmark. The rate counts the prompt tokens processed during proof generation. It excludes setup and commitment creation, and a request waits for the batch. Verification adds further work.

The technical report puts proving at roughly 70 to 95 times ordinary inference in GPU time under its comparison conditions. That is substantial overhead even if it represents progress for cryptographic proofs. It would be misleading to compare the headline rate directly with an API's output-token speed.

What a proof still cannot tell you

The technical report describes proofs generated after inference through recomputation. This can reveal tampering after a response is served; it does not necessarily stop that response reaching a user first. For a system that immediately acts on model output, the timing of the check matters as much as its eventual result.

There are also numerical limits. The strict claim concerns an integer model and greedy token choices. Normal floating-point inference or sampling can produce different tokens without anyone substituting a model.

The project's known limits distinguish exact matching from a more permissive policy that tolerates differences. Acceptance under that policy means the output meets its chosen limits, not that it exactly reproduces the model's output. Only the specified token positions are covered.

Formal verification also has a boundary. The Lean protocol and verifier have machine-checked properties. The fast C++ verifier and CUDA prover are tested implementations, not themselves formally proved. The repository reports no independent security audit.

Where this could become useful

I think the immediate opportunity is targeted assurance: checking a consequential evaluation or a particular inference claim where the extra computation can be justified. Trying to prove every ordinary chat response would face very different economics.

Even a perfectly implemented proof would establish a computation, not the truth or usefulness of its answer. An authentic model can still be wrong. The next meaningful step is showing that these guarantees survive realistic serving conditions, with enough context and affordable overhead to support decisions people actually make.

I’m Paras. I work at the intersection of AI, engineering and distribution.

I help technical founders turn research and product launches into clear stories that developers can understand and share.

Book a 30-minute call.