Seven of Ninety-Six Scout Replies Met the Limits

On 2 November Anthropic published “Progress on provable inference for large language models,” with code, Lean proofs and a technical report under Apache 2.0. The system is called FlashProve. It lets a model provider commit to a set of weights and then attach a zkSNARK to a response, a proof that the committed weights produced it, which anyone can check on a CPU without seeing the weights. The headline result is Llama 4 Maverick, a 400B-parameter mixture of experts in 4-bit weights, proved on a single H100 at about 110 tokens per second, with a proof of about 19 MB per 1,024-token request, at roughly 70 to 95 times the GPU time of running the model on vLLM.

The post opens with the problem it wants to solve. A user today can’t check that a response came from the model they asked for, “as opposed to one secretly substituted in by a routing service for cost reasons.” That is the case I wanted to test against the release. The blog post is short. The repository, version 0.16.0, has some of the most careful self-reporting I have read in a research release, and it answers the substitution question more narrowly than the headline does.

The progress is real

Start with what isn’t in dispute. The post’s own survey of prior work puts the gain in perspective. zkLLM in 2024 proved a 13B model at about 2.5 tokens per second in a batch, on one A100. The only earlier proof of Maverick the authors know of, VerInf, reports 14.3 hours for 1,000 tokens, with a 93.6 GB proof “which took almost a day to verify.” Attestable, a commercial effort, reports 53 to 77 tokens per second on a dense 31B model, with no open-source release.

Reported proving throughput for language model inference, log scale Log-scale bar chart of tokens per second as reported in Anthropic's survey of prior work. VerInf proved Llama 4 Maverick at about 0.02 tokens per second, 14.3 hours for 1,000 tokens. zkLLM in 2024 proved a 13B model at about 2.5 tokens per second in a batch on one A100. Attestable reports 53 to 77 tokens per second on a dense 31B model, not open source. FlashProve proves Llama 4 Maverick at about 110 tokens per second on one H100. PROVING THROUGHPUT, TOKENS PER SECOND, LOG SCALE · ANTHROPIC, 2 NOV 2026, PRIOR WORK 0.01 0.1 1 10 100 1,000 VerInf, Maverick 400B zkLLM (2024), 13B, batch Attestable, dense 31B FlashProve, Maverick 400B 14.3 h per 1,000 tokens one A100 one H100, not open source one H100, open source About 0.02 tokens/s (14.3 hours for 1,000 tokens) — VerInf, as cited by Anthropic, 2 Nov 2026 About 2.5 tokens/s in the batch — zkLLM (2024), as cited by Anthropic 53 tokens/s, low end of 53–77 — Attestable, as cited by Anthropic About 110 tokens/s — FlashProve, Anthropic, 2 Nov 2026 Range up to 77 tokens/s — Attestable, as cited by Anthropic ≈0.02 ≈2.5 53–77 ≈110 Different models, hardware and counting rules; read as orders of magnitude, not a like-for-like benchmark.
Against the only earlier proof of the same model, the jump is more than three orders of magnitude. Whatever follows, that part holds.

The security claims also come with machine-checked backing. Soundness is proved in Lean for a Lean verifier: a false claim gets through with probability about q/2^124 + 2^-101 after q hash queries, in the random-oracle model. The fast C++ verifier people actually run is tested against the Lean one, not proved. The authors say so. They also call the release a research prototype: “This research post is meant to share intermediate progress, and not a completed research agenda.”

What the 110 counts

The repository’s performance page is precise about what the headline rate measures. These are “steady prefill rates: each request’s 1,024 prompt tokens count, nothing is generated.” Each proof states one token, the next one after the window. The page’s own warning on the cost ratios: “a pass checks one token, so this is not the cost of proving a generated reply.”

The page does report the rate with whole replies checked. Under the looser policy described below, at 24 requests a batch, it is 108.67 tokens per second counting all 1,024 positions, or 39.1 counting reply tokens alone.

FlashProve throughput by what is counted Bar chart of measured rates on Llama 4 Maverick on one H100. At 24 requests per batch, prefill with one next token stated per proof runs at 111.23 tokens per second. At one request per batch the same measure is 17.41. With whole stored replies checked under the clipped-gap policy, the rate is 108.67 tokens per second counting all 1,024 positions, and 39.1 counting reply tokens alone. TOKENS PER SECOND, ONE H100, MAVERICK 4-BIT · FLASHPROVE GUIDE/PERFORMANCE.MD, V0.16.0 Prefill, 24 per batch Prefill, 1 per batch Whole replies, all positions Whole replies, reply tokens only one next token stated per proof one next token stated per proof 24 per batch, clipped-gap policy same run 111.23 ± 0.92 tokens/s — FlashProve performance page 17.41 ± 0.15 tokens/s — FlashProve performance page 108.67 ± 2.8 tokens/s — FlashProve performance page 39.1 ± 1.0 reply tokens/s — FlashProve performance page 111.2 17.4 108.7 39.1 Start-up and the 39-minute commitment are not counted. Whole-reply runs used 524-token prompts and stored replies of 31 to 500 tokens; no inference engine ran.
The prover's work tracks the 1,024-token window. How much of the window is the model's reply decides whether the useful rate is about 110 or about 39.

That’s a fair way to report a prover, and the release is open about it. But it means the 70-to-95-times figure is a prefill comparison. Against decoding, the repository puts one pass at 20.1 times slower than vLLM generating as many tokens at 512 streams, and then reminds you again that the pass checks one token.

Two policies, and the theorem covers one

The more important split is between two acceptance policies.

Exact match accepts a reply only if every checked token is the top choice of the committed model. That model is an integer version of the weights, quantized and fixed-point, because a proof system works over integers. This is the policy the Lean soundness theorem covers.

The trouble is that nobody serves the integer model. The repository measured how often its top token differs from the 16-bit weights evaluated in float32: at 5,779 of 84,893 positions in 216 texts, or 6.81 percent. Most of that gap is already present in the third-party 4-bit conversion before any integer arithmetic, which differs from the 16-bit weights at 6.65 percent of the same positions. A reply of a few hundred tokens gives that rate a lot of chances to show up. By the project’s scoring, “of the 96 honest replies scored† from each of two stock engines none would pass exact match,” one at 16 bits and one at FP8. The dagger marks results that were not produced on the released programs.

This lines up with what quantization studies keep finding. Huang and colleagues evaluated ten post-training quantization and LoRA fine-tuning methods on LLaMA3 from 1 to 8 bits, and found it “still suffers from non-negligible degradation,” worst at ultra-low bit widths. The 6.81 percent disagreement comes from 4-bit weights, and FlashProve inherits it. It means the exact-match theorem has nothing to say about an ordinary served reply.

So serving uses a second policy, called clipped gap. It scores each checked token by how far it falls below the integer model’s top choice, clips each cost, and accepts if the average and the count of costly tokens stay within limits fitted on honest replies. A pass prints WITHIN LIMITS instead of YES, and the known-limits page puts it plainly: “WITHIN LIMITS does not say the reply is the model’s.” Under that policy Lean proves only that the reply meets the policy. The paper argument covers its equations “only in part.” Both outcomes exit with code 0.

What the looser policy lets through

Share of replies accepted under each policy Bar chart of acceptance rates reported in the FlashProve repository. Under exact match, 0 of 96 honest stock vLLM replies at 16 bits and 0 of 96 at FP8 would pass, by scoring. Under the clipped-gap limits, 127 of 128 fresh honest Maverick replies got an accepted proof, 99.2 percent. By scoring, 28 of 32 replies with one token swapped for the model's second choice met limits fitted to honest replies, 87.5 percent, and 7 of 96 greedy replies from the smaller Llama 4 Scout met the limits, 7.3 percent. SHARE OF REPLIES ACCEPTED · FLASHPROVE GUIDE/KNOWN-LIMITS.MD, INTEGRATIONS/LIMITS.MD, V0.16.0 EXACT MATCH · COVERED BY THE LEAN SOUNDNESS THEOREM CLIPPED GAP · THE POLICY SERVING USES Honest replies, stock vLLM, 16-bit Honest replies, stock vLLM, FP8 Fresh honest Maverick replies One token swapped for 2nd choice Greedy replies from Llama 4 Scout 0 of 96 would pass, scored — known-limits.md 0 of 96 would pass, scored — known-limits.md 127 of 128 got an accepted proof (99.2%) — integrations/LIMITS.md 28 of 32 met the limits (87.5%), scored, not proved — known-limits.md 7 of 96 met the limits (7.3%), scored, not proved — integrations/LIMITS.md 0 of 96 0 of 96 127 / 128 28 / 32 7 of 96 Only the 127 of 128 are proofs. The rest were scored by a Python package. In a proved run, 0 of 24 Scout replies got a proof. Refitting the limits on 200 other draws gave a median of 1 of 96 Scout replies through (least 0, most 10).
The policy the theorem covers accepts no stock replies at all. The policy that accepts honest replies also lets through some from a cheaper sibling of the committed model.

The honest side looks good. Of 128 fresh greedy replies from stock vLLM, under limits fixed before any of them was served, 127 got an accepted proof. The release counts the other side too. Replies with one token swapped for the model’s second choice met the limits in 28 of 32 cases. By stored costs, “nearly all” replies Maverick gave when served in FP8 met them, as did all those served with top-p 0.9 and most of those sampled at temperature 0.7 or 1. And 7 of 96 greedy replies from Llama 4 Scout, a smaller model in the same family, met the limits they shouldn’t have.

Those are scored results, not forged proofs. In the proved run, none of 24 Scout replies got a proof. The authors say the Scout test “does not show that the limits tell models apart in general,” and that “No run shows the clipped-gap policy’s own limits rejecting anything at a verifier.” Refitting the same rule on 200 other draws of honest replies gave a median of 1 Scout reply in 96 getting through, with a range of 0 to 10. The limits in the release sit on the loose side of what the rule produces.

Put that next to the motivating case. A routing service secretly swapping in a cheaper model from the same family is the attack the post leads with. Under exact match, the release can’t certify honest stock serving. Under clipped gap, it certifies honest serving and lets some of the cheaper model’s replies through, how many depending on how the limits were fitted. The repository’s own recommendation is blunt: “The project recommends no limits: if you cannot assess them, accept only exact match.”

Both policies also rest on an earlier condition. A proof binds a reply to a commitment, not to a name. “A provider can commit to any model it likes,” the known-limits page says, and a user should get the commitment ID “from a party you trust,” never from the server being checked.

Where the theorem and the deployment can meet

In 1986 Goldreich, Micali and Wigderson showed how general zero-knowledge proofs are, when they were known only for a few number-theoretic problems. In 2020 Zhang and colleagues set out to “initiate the study of zero knowledge machine learning,” starting with decision trees. What was missing was a version cheap enough to run at frontier scale, and FlashProve gets most of the way there on cost. The part still open is that the model being proved has to be the model being served.

The repository has a route to that. Through vLLM with a plug-in designed to compute the integer model exactly, 48 of 48 short replies were proved and checked, on synthetic prompts and in runs not on the released programs, serving at 0.58 to 1.46 seconds per token. That is slow, but the exact-match theorem covers it. If a provider served the integer model itself, the honest-reply problem would go away. So would the need for fitted limits, and with them the Scout leak.

For the goal Anthropic set in its RSP updates, a prototype by 30 September 2026 that signs model outputs “in a way that makes them attributable to a specific set of model weights,” Anthropic says it met it through “a separate but related project, which signs our inference traffic and recomputes inference on a trusted server.” FlashProve is the cryptographic route to the same goal, and it isn’t finished.

I wrote last month that when Anthropic proved 239 fuzz entry points crash-free, the theorems were real and their reach was set by whoever wrote the fuzz test. Here the reach is set by the acceptance policy. The exact-match proof is real, and so are the 110 tokens per second. But exact match accepted none of the 96 stock replies, and the policy that does accept them let 7 of 96 Scout replies through.

References

  1. Anthropic (Rinberg, R., Allain, A., Chiesa, A., Christ, M., Dalal, R., Fenzi, G., Mayer, B. and Weissenberg, G.) (2026). Progress on provable inference for large language models. Published 2 November 2026.
  2. Anthropic (2026). FlashProve, version 0.16.0, Apache 2.0, repository as of 30 October 2026: guide/performance.md, guide/known-limits.md, guide/what-is-proved.md, docs/limits.md, integrations/LIMITS.md.
  3. Sun, H., Li, J. and Zhang, H. (2024). zkLLM: Zero Knowledge Proofs for Large Language Models. arXiv:2404.16109, submitted 24 April 2024.
  4. Goldreich, O., Micali, S. and Wigderson, A. (1986). Proofs that yield nothing but their validity and a methodology of cryptographic protocol design. 27th Annual Symposium on Foundations of Computer Science (FOCS 1986): 174–187, October 1986.
  5. Zhang, J., Fang, Z., Zhang, Y. and Song, D. (2020). Zero Knowledge Proofs for Decision Tree Predictions and Accuracy. Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security: 2039–2053, 30 October 2020.
  6. Huang, W., Zheng, X., Ma, X., Qin, H., Lv, C., Chen, H., Luo, J., Qi, X., Liu, X. and Magno, M. (2024). An empirical study of LLaMA3 quantization: from LLMs to MLLMs. Visual Intelligence 2: 36, published 30 December 2024.