Anyone who regularly uses large language model APIs or official subscriptions tends to harbor two suspicions. First, third-party API relays might swap out top-tier models for cheaper or stripped-down alternatives to cut costs. Second, major AI labs might quietly degrade model quality during peak compute hours to save capacity. Until now, neither suspicion could be proven: looking at text outputs alone cannot confirm which model produced them, proprietary weights are kept behind closed doors, and ordinary users do not have hundreds of GPUs lying around to reproduce the run.
On November 2, Anthropic open-sourced FlashProve, a provable inference prototype that essentially acts as a mathematical bill validator for AI. Even without seeing the model weights or owning a GPU, you can run a 17-second check on an ordinary CPU to mathematically verify which model generated a given response. Yet a closer look at the accompanying 23-page technical report reveals a sharp divide: this validator can catch third-party relays swapping models red-handed, but it cannot police a major provider quietly degrading its own service.
Many developers react to provable inference with immediate skepticism: if the model weights remain secret and the user’s computer has no GPU, how can an ordinary processor tell whether a remote server cooked the books? FlashProve brings in zero-knowledge proofs, a cryptographic technique that proves a calculation was carried out faithfully without exposing the underlying proprietary weights. The entire anti-counterfeiting workflow breaks down into two steps.
In the first step, the provider seals the model offline. Running a commitment program over hundreds of billions of weight parameters for 39 minutes produces a public weight fingerprint of roughly 6 MB. Changing even a single parameter yields a completely different fingerprint, yet the fingerprint itself reveals nothing about the weights.
In the second step, the provider issues a receipt alongside the output. While processing a request, the server packages the arithmetic results and token selection at every layer into a proof file of about 19 MB. Once the user receives this cryptographic receipt, running a verification program for 17 seconds on a 24-core CPU spot-checks the mathematical interlocking across layers. If any step swapped weights or skipped computations, the numerical chain inside the receipt breaks.
This makes after-the-fact ticket forging impossible for a relay. Suppose a relay normally serves a cheap model that outputs Answer A, and only runs the real model when audited to generate a proof on the fly. Mathematically, that hits a dead end: the proof file binds the input prompt, the weight fingerprint, and the exact output together. Even if the real model’s Answer B differs from Answer A by a single punctuation mark, it cannot produce a valid proof pointing to Answer A. Similarly, if a relay silently truncates a long prompt or injects a hidden system instruction asking for brief replies, running the verifier against the user’s original prompt will fail right at the first layer.
Of course, printing this mathematical receipt is not cheap. Generating a proof consumes 70 to 95 times more compute than running standard inference on an open-source engine like vLLM. Nobody will generate a receipt for every sentence in daily chat; the realistic use case is post-hoc spot auditing. As long as an enterprise buyer or benchmark organization reserves the right to audit a small fraction of requests in its contract, the relay never knows in advance which queries will be inspected. Getting caught once leaves irrefutable cryptographic evidence, making the penalty for breach of contract far outweigh the electricity saved by swapping models.
Even at nearly a hundred times the cost of raw inference, building FlashProve was a formidable engineering feat. Anthropic benchmarked the system on Meta’s open-weight Llama 4 Maverick; among prior open-source systems, only VerInf had ever produced a proof for a model of this scale, taking 14.3 hours on a high-end server to finish a single benchmark run, outputting a 93.6 GB proof file, and requiring nearly a full day just to verify.
By contrast, FlashProve pushes proving speed on the exact same model to 110 tokens per second on a single GPU, improving both speed and proof size by roughly 5,000x. Hitting that throughput on a single card came down to two hardware-aligned engineering trade-offs.
The first strategy embraces the sparsity of Mixture-of-Experts models and proves only the parameters actually used. Although Llama 4 Maverick totals 400 billion parameters across 128 routed experts per layer, processing any single token activates just one routed expert plus a shared expert, meaning only 17 billion parameters participate in the math.
When generating a proof, FlashProve writes only the computation of that single active expert into the receipt while using cryptographic blinding to hide which expert index was chosen. Prover workload scales with active parameters rather than total parameters, eliminating over 90% of wasted proving work. Combined with keeping the 232 GB model weights in host RAM and streaming them layer by layer into 80 GB of GPU memory, a single H100 GPU can run the entire pipeline.
The second trade-off abandons token-by-token proving during generation and instead recomputes the whole passage in parallel after the response finishes. Online LLM inference has two distinct phases: prefill, where the model reads the entire input prompt at once and is bound by GPU compute, and decode, where it emits the reply one token at a time and is bottlenecked by memory bandwidth. Proving each token as it streams out would fight online decoding for memory bandwidth and grind serial generation to a halt.
FlashProve decouples the two: the production server returns the answer to the user as usual, while a separate proving server recomputes the full conversation history in the background. Because the entire reply already exists, the proving server treats the prompt plus the reply as one combined prefill pass in parallel, batching 24 requests together so the weight commitment only needs to be unpacked once per batch. Re-running the model forward pass accounts for just 1% to 1.5% of total proving overhead, unlocking massive parallel throughput.
In the technical report, the authors also explain the exact accounting behind that headline speed. Although the prover can verify any number of output tokens, it must still compute over the entire 1,024-token window of inputs and outputs. The default official benchmark therefore verifies only the first token immediately following the prompt, then divides the full 1,024-token window by the wall-clock time to report throughput. Switching to full-verification mode, where every generated reply token is checked, barely changes total runtime; however, counting only the verified reply tokens in the numerator brings the effective speed to 39.1 tokens per second.
Once developers understand how the mechanism works, the most natural question follows: can we point this validator at Anthropic itself to test whether Claude gets dumber during peak hours? Three technical details in the report explain why that remains out of reach.
The first hurdle is the inherent gap between online floating-point math and the prover’s integer model. Production clusters run floating-point formats like FP8 to balance accuracy and speed. Because GPU floating-point addition is not associative, changing batch sizes or chip architectures introduces tiny numerical jitter, making direct mathematical proofs impossible. To sidestep this deadlock, FlashProve actually proves an integer-quantized shadow model.
The catch is that even when the provider acts in complete good faith, the tokens emitted by the online floating-point model and those computed by the post-hoc integer shadow model will naturally diverge whenever top candidate tokens have nearly identical scores. The report’s appendix bridges this gap by adding a statistical check based on near-ties: if the discrepant token happens to be a close runner-up or third-place candidate in the integer model, the verifier waves it through as normal floating-point noise. By design, that tolerance window leaves room for subtle precision loss.
The second barrier is that the protocol locks in greedy token selection and a short 1,024-token window, leaving hidden chain-of-thought budgets untouched. To keep recomputation deterministic, the protocol requires picking the highest-scoring token at every step (greedy decoding), effectively locking sampling temperature at zero. In real-world coding or reasoning tasks on Claude, contexts routinely span hundreds of thousands of tokens. Moreover, peak-hour degradation rarely involves swapping base weights; instead, the server might cap the token budget allowed for hidden reasoning or truncate long context histories. As long as hidden reasoning chains are not disclosed in full and included in the proof window, a 1,024-token check cannot reach them.
The third barrier is that the weight fingerprint must be rotated every 16 million requests. To prevent outsiders from harvesting enough proofs to reverse-engineer the secret weights, each offline weight commitment safely covers at most 16 million queries before a fresh commitment is needed. For a frontier lab, that quota burns out in a matter of hours. If an official provider simply publishes a brand-new root fingerprint alongside a routine minor update, cryptography can only confirm that today’s responses match today’s fingerprint; it cannot guarantee that the model behind the new fingerprint wasn’t scaled back compared to last month’s version.
Beyond algorithmic boundaries, version 0.16.0 of the prototype carries a fascinating implementation twist. The underlying cryptographic math is intricate enough that hand-writing low-level C++ invites subtle security bugs that human cryptographers can easily miss during manual review. So the team flipped the workflow: they first wrote the core anti-counterfeiting rules as a mathematical master specification in Lean, a theorem-proving programming language. Lean’s compiler acts like an unforgiving grading machine; once the code compiles, the top-level soundness theorem is mathematically guaranteed to hold without logical loopholes.
Next, they had Claude automatically translate that Lean master specification into the GPU C++ prover, the CPU C++ fast verifier, and even the long-form protocol specification document inside the FlashProve open-source repository. The human authors candidly note in the report that the long-form protocol document has not been thoroughly reviewed, nor have they formally proven equivalence between the translated C++ code and the Lean specification. That raises an obvious question: if you use AI-translated code that the authors themselves haven’t fully audited to catch cheating, what happens if Claude mistranslated a step?
Why could the team take that gamble safely? By separating the duties of the prover in the provider’s data center from the verifier on the user’s machine, they cleanly isolated the three possible failure modes of an AI translation bug. The first failure mode is an arithmetic bug in the server-side C++ prover that causes receipts from genuine model runs to fail verification. That has nothing to do with adversarial cheating; running standard software tests on normal queries immediately exposes any receipt that fails to verify.
The second failure mode is the prover accidentally dropping random blinding masks during batching or C++ translation, causing receipts to leak information about the secret model weights. Right now, the team’s Lean specification only proves zero-knowledge privacy for single queries, leaving batched privacy proofs incomplete, and the Lean code itself cannot run proving directly across hundreds of billions of parameters. However, any weight leakage only harms the provider’s own trade secrets rather than tricking users into accepting fake answers. Because this open-source demo runs on Meta’s publicly released weights, weight leakage carries zero risk here. Any commercial lab adapting the tool for proprietary models would need to complete the batched proofs and hire security auditors to inspect the prover code.
The third failure mode, and the only one users care about, is whether a dishonest provider could exploit a code flaw to forge a fake receipt that fools the user. That cannot happen because the user’s local verifier holds sole authority over whether a receipt is accepted. As long as the verifier on the user’s computer is sound, even a buggy or maliciously modified prover on the server cannot fabricate a passing receipt. What if the C++ fast verifier in the user’s hands has a translation bug? Because verification requires very little compute, the team built a double safeguard: alongside the C++ fast verifier, they compiled the mathematically checked Lean master specification directly into a pure Lean slow verifier. Routine spot checks can run on the C++ fast verifier while cross-checking it against the Lean verifier on test suites; for formal compliance audits, legal disputes, or any doubts about the C++ translation, auditors can bypass C++ entirely and run the pure Lean slow verifier. That completely removes AI translation errors from the trust boundary.
A footnote in the research blog also reveals how Anthropic handled its own internal deadline. Earlier safety roadmaps set a September 30 target for building a prototype that verifies inference traffic. As the footnote explains, Anthropic fulfilled that internal milestone with a much simpler design: cryptographically signing inference traffic and re-running it on trusted internal servers to guard against hackers compromising production machines or stealing weights.
Seeing how those two tracks divide the labor clarifies where FlashProve truly fits in the ecosystem. Carrying a 70x to 95x compute premium means it will not become a real-time toggle that everyday users flip on for casual chats; instead, it serves as a post-hoc spot-auditing weapon hanging over compute hosts, third-party API relays, and benchmark submitters. Once buyers or evaluation boards gain the power to demand cryptographic verification on a small random sample of past queries, the black-box API era, where users had no choice but to trust a provider’s word, changes its rules of engagement.