Anthropic open-sources FlashProve, a zkSNARK system for verifying LLM responses

Anthropic, working with academic collaborators from EPFL, MIT, StarkWare and Succinct, has released FlashProve, an open-source prototype for "provable inference": cryptographic proofs that a language model's response was actually produced by the specific model a provider claims to be serving. According to Anthropic's research post, the system is fast enough to be practical, generating proofs at roughly 110 tokens per second for a 400-billion-parameter model on a single H100 GPU.

The verification gap

The post describes a problem that is easy to overlook: nothing in a model's output tells you which model produced it. A third-party routing service could quietly substitute a cheaper model to cut costs, and an attacker tampering with the token stream would be just as hard to detect from the response alone. For casual use this may not matter much, but Anthropic argues it does matter for independent evaluators who test models before and after release, for customers paying for a particular model, and for anyone who needs assurance that a served model has not been swapped.

Verification is structurally difficult: frontier model weights are private, and even a user who had the weights would need substantial compute to re-run the model and check a response. Provable inference is meant to let someone with modest resources and no knowledge of the weights confirm that a response came from the committed model.

zkSNARKs applied to inference

FlashProve is built on a class of cryptographic proof called a zkSNARK, or zero-knowledge succinct argument of knowledge. The provider commits to a model up front, then attaches a short certificate to each response. That certificate can be checked quickly — ideally in seconds on an ordinary CPU — fails if the response deviates from the committed model, and, being zero-knowledge, reveals nothing about the weights. Anthropic notes that hiding the model's architecture is deliberately not a goal of the system.

The headline numbers, per Anthropic: for Llama 4 Maverick, a 400-billion-parameter mixture-of-experts model running with 4-bit quantized weights and integer arithmetic in prefill, one H100 GPU produces proofs at around 110 tokens per second, with proof sizes of about 19 MB per 1,024-token request. Generating proofs takes roughly 70 to 95 times the GPU time that vLLM, a common open-source inference library, needs to process prompts of the same length. Anthropic says prior open-source provable-inference systems lag far behind, by orders of magnitude.

Claude built much of it, and Lean checks the claims

A striking detail of the release is who did the engineering. Anthropic credits Claude, its own model, with the improvements to zkSNARKs, saying it found new ways to apply state-of-the-art tools from the cryptography and security literature while sticking to well-established design principles for proof systems. Because an AI optimizing a large system makes many choices that are hard for humans to evaluate, the team anchored its security claims in Lean, a formal verification language: the top-level mathematical statements come with machine-checked proofs and an interactive visualizer to aid auditing.

Five artifacts shipped together: the blog post, a technical report, a protocol specification, executable code containing a prover and two verifiers (a fast C++ verifier and a provably correct Lean verifier), and the Lean proofs themselves. Everything is available under the Apache 2.0 license. Anthropic is explicit that this is intermediate progress rather than a completed research agenda, and says it is releasing the work in the hope that others take it and improve on it.

Why it matters

If provable inference becomes cheap enough, model identity stops being a question of trust and becomes something checkable. Auditors could confirm they are evaluating the model actually being served, customers of routing services could verify what they paid for, and providers could demonstrate compliance with compute-usage commitments. Anthropic specifically points to AI pacing and regulation proposals that rely on monitoring hardware use — for example, a provider required to devote its hardware to inference rather than training a new model could face pressure to cheat, and cryptographic proofs give a regulator a way to check. FlashProve's overhead is still significant at 70 to 95 times the cost of plain inference, but that is within a range where selective, high-assurance use is plausible. The release also demonstrates a workable pattern for AI-assisted engineering of security-critical systems: let the model do the optimization, then formalize and machine-check the guarantees that people actually rely on.