Anthropic — Progress on Provable Inference for Large Language Modelsauto-ingested

Anthropic's Frontier Red Team releases FlashProve, an open-source prototype that attaches a cryptographic proof (a zkSNARK) to a model's output, showing the response came from a committed set of weights without revealing them. Claude built much of it; Lean proofs back the security claims. It is the wiki's first source on verifying what an AI did without trusting or re-running it, which makes it a counterpoint to Verification Requires Domain Knowledge. Subscribed-feed capture (Anthropic Research), auto-fetched and auto-ingested 2026-11-08; awaiting human review.

The problem

A user "cannot check that the responses came from the specific model that a developer claims is responding." A router might swap in a cheaper model, or an attacker might tamper with the token stream. Judging by output quality is unreliable. Checking by re-running would need the private weights and frontier-scale hardware. The goal of provable inference (PI) is to let a user "with limited computational resources and without any information about the weights" verify that a response came from the requested model.

Four trust challenges PI addresses

1. Pacing. Proposals to pace AI development (the post links Dario Amodei's "We must pace the frontier") may require providers to devote hardware to inference rather than training. Proofs for the served requests show the hardware really served the claimed model. The post flags the limit itself: this "does not establish that the hardware is not, e.g., training on the side."
2. Tamper detection. A compromised inference server, or "a more advanced model [running] in place of the one that was authorized and present[ing] itself as the weaker model," cannot produce valid proofs for the expected weights.
3. Text provenance. Prove a claimed analysis was really done by a given model, e.g. a library scanned by a frontier security model. Includes a "Proof-of-Failure": proof that a provider spent at least X tokens on a specific model and did not find a bug in a patch.
4. Model approval. A regulator can require proofs so that only approved models are served.

Trusted hardware (TEEs) is the main alternative. The post presents it as complementary: TEEs trust the manufacturer; cryptographic proofs rest on "the hardness of computational problems," even if hardware and OS are compromised.

How FlashProve works

• Two parties, two phases. Offline, the provider publishes a short commitment that pins down one exact set of weights while hiding them. Online, for each request, it produces a proof of the statement "The committed model produces these output tokens when evaluated."
• Four guarantees: completeness (honest proofs verify), soundness (false proofs effectively can't be forged), zero-knowledge (nothing leaks about the weights, intermediate values, or which experts ran; the architecture is not hidden), and succinctness (small, cheap to check). The first two alone are trivial for a verifier who has the weights and a GPU. The last two make it useful.
• Construction: an interactive oracle proof (IOP) compiled with hash functions into a zkSNARK, the same family deployed in Ethereum L2s (Starknet, Mantle); post-quantum secure.
• Design choices: prover work scales with the ~17B active MoE parameters, not all 400B; requests are proved post-hoc in batches (prefill-style), not in-line; weights stream from host memory so one 80 GB GPU (~290 GB host RAM) suffices.

Numbers (Llama 4 Maverick, 400B MoE, 4-bit)

Offline commitment	~39 min once per model; good for ~16M requests
Prover throughput	~110 tokens/s on one H100 (24 requests in ~223 s)
Proof size	18.78 MB per 1,024-token request
Verifier	17 s on 24 CPU threads (21 s single-thread); commitment download ~6.5 MB; no GPU
Overhead vs vLLM	~72× per GPU (66–77 across runs); ~94× vs vLLM at highest load

Prior art, for scale: zkLLM (2024) ~2.5 tok/s batched on a 13B model; VerInf proved the same Maverick model at ≈0.02 tok/s, with a 93.6 GB proof that took almost a day to verify; DeepProve 1.4–2.9 tok/s single-machine; commercial Attestable 53–77 tok/s on a dense 31B model (not open source). The authors' conclusion: overhead of "roughly 2 orders of magnitude… much less than previously expected," and the progress "should update our priors on what it is possible to prove in zero-knowledge."

Claude built it, so they proved it

• "Claude has produced improvements on zkSNARKs for inference" and "found novel ways to apply state-of-the-art tools." The protocol specification is Claude-written.
• The key caveat: "Claude is good at optimization, but often makes decisions that are hard to evaluate, especially in large complex systems." Their counter is "top-level auditable statements in Lean" for the security guarantees.
• Formal verification leaves two trust gaps, which the post names:
  1. The formal statements must be audited by hand to check they mean what is intended. This is "dramatically less onerous than auditing proofs"; they ship an interactive visualizer to help.
  2. The executable code must match the formally specified protocol. Here the verifier/prover asymmetry does the work: soundness depends only on the verifier ("the entire value of having 'proofs' is that you can fully distrust the prover if you trust the verifier"), so they ship a slow, provably correct Lean verifier next to the fast C++ one. Zero-knowledge depends only on the prover, which is too expensive to run in Lean, so that part is left to "careful agentic and/or human security audits."

Limitations (from the post)

• No formal guarantee that the fast code, the paper and the Lean protocol match.
• Proves an integer model under greedy decoding. Floating-point or sampled output can diverge; adversarially designed prompts are not covered.
• Assumes MoE; does not hide architecture; side channels (e.g. proving time) out of scope.
• Contexts capped at 1,024 tokens, far below frontier context windows.

Context: Anthropic's roadmap goal

Anthropic's Frontier Safety Roadmap set a public goal of a provable-inference prototype by 2026-09-30. It says it met that goal through a separate project that signs inference traffic and recomputes inference on a trusted server. FlashProve pursues the same aim by cryptography. In an October 19, 2026 update the goal was renamed "inference verification", because "provable inference" suggested a narrower approach than needed.

Key claims

• Cryptographic PI for a 400B model is ~70–95× native GPU cost, with ~19 MB proofs checkable in seconds on a CPU. Earlier systems were orders of magnitude slower.
• Proofs bind outputs to a weight commitment while revealing nothing about the weights.
• Claude-built cryptographic systems need formal statements because Claude's design choices are "hard to evaluate"; auditing statements is far cheaper than auditing proofs, but still manual.
• A proof that the hardware served inference is not a proof that it did nothing else.

Connections

• Provable Inference — the concept page this source opens.
• Verification Requires Domain Knowledge — the counterpoint: a design where the checker needs neither the weights nor the derivation, only a trusted verifier and an audited statement. It narrows that page's claim without refuting it.
• Control-Flow Integrity — the wiki's other software-security page. Both enforce a pre-committed specification against an adversary who controls the runtime; the cost gap (CFI ~16%, PI ~70–95×) shows how much more expensive proving is than checking in-line.
• Falsification Is Asymmetric — the "Proof-of-Failure" certifies effort spent, not the absence of bugs; one probe can disprove "never," and a million tokens of failing to find one cannot prove it.
• Token Shortage — a ~72× compute multiplier is why proving is post-hoc and sampled, not on every token.
• AI-Accelerated Science — another case of Claude producing research-grade improvements, here in applied cryptography, with the evaluation problem handled by formal methods rather than wet-lab ground truth.
• AI Use Tracks AI Capability — Claude excelled at the measurable part (optimization), and the hard-to-evaluate part needed an external checker.
• Dario Amodei — his "We must pace the frontier" post is cited as a motivation.
• Anthropic — Frontier Red Team; roadmap goal; inference-verification renaming.
• Method Reflection — T3: "audit the statement, not the derivation" as a review-economy counterweight.

Source

• Original: raw/2026-11-02 Anthropic — Progress on provable inference for large language models.md (anthropic.com/research/provable-inference). Companion artifacts not ingested: the technical report, the Claude-written protocol spec, the FlashProve code and Lean proofs (github.com/anthropics/FlashProve), and the related post "LLMs are making formal software verification feasible at a much larger scale" (Frontier Red Team, 2026-10-22) — a reading lead.