FlashProve: Verifying LLM Outputs Match the Specified Model Without Revealing Weights

Lock the Model First, Then Verify Each Inference

FlashProve splits the process into an offline phase and an online phase. In the offline phase, the service provider generates a short hidden commitment for the model weights — a cryptographic fingerprint that prevents undetectable substitution. The client stores this commitment without needing to download terabyte-scale weights.

In the online phase, the provider must prove that the returned tokens were produced by the committed model. Two guarantees are central: honest correct inference passes verification, while weight substitution or forged computation is practically impossible to slip through. The proof reveals neither the weights nor the intermediate computation trace.

Turning Massive Computation into a Random Spot-Check

Because the verifier cannot re-execute the entire computation, FlashProve first uses an interactive oracle proof to encode the computation with redundancy, then detects errors via a small number of random queries. A Merkle commitment compresses long messages into a short digest, and the Fiat–Shamir transform folds multiple interaction rounds into a single proof. This chain relies on relatively basic cryptographic primitives such as BLAKE2 hashing. The paper provides a security analysis in the random oracle model and positions the scheme as a succinct zero-knowledge proof with post-quantum security potential. The client sees only a quickly verifiable proof, not the full computation.

Why the 400B Model Chooses MoE First

Experiments use Llama 4 Maverick, a ~400 billion parameter model with 128 experts. Each token activates only one routed expert and one shared expert per MoE layer, so only ~17 billion parameters are actually used. This sparsity lets the prover record only the activated experts' computation traces and verify that routing decisions were correct. Sparse activation reduces both inference cost and the amount of computation that must be encoded and proven. For non-linear operations the system uses lookup tables; for numeric computation it employs exact integer-quantized models, avoiding floating-point non-determinism across hardware.

Lean Adds a Layer of Verification to the Cryptographic Proof

FlashProve not only specifies the protocol but also uses Lean to formalize the correct inference relation, prover and verifier algorithms, and the properties of completeness, soundness, and zero-knowledge with concrete error bounds. The paper provides a verifier directly compiled from Lean. A higher-performance C++ version is generated by an AI agent from the Lean representation, but the two have not yet been proven formally equivalent. Thus the mathematical protocol has reached machine-checked verification, while end-to-end implementation equivalence remains to be closed.

The Real Breakthrough Lies in These Engineering Numbers

The prover runs on a single H100 GPU, 24 CPU cores, and host memory. The 232 GB weights are streamed in batches into 80 GB VRAM. With a batch of 24 requests, proof generation takes ~223 seconds, yielding 110 tokens/second throughput. In single-request mode, proof generation takes ~58 seconds, dropping throughput to 17.6 tokens/second. Each online proof is 18.78 MB. The client needs no GPU: verification with 24 threads takes ~17 seconds, single-threaded ~21 seconds. The key deployability milestone is that a 400B model proof runs on a single GPU system, while an ordinary computer can verify independently.

The cost is equally clear: in batch mode each request waits about five minutes; per GPU, proving takes ~72× the time of a normal prefill, rising to ~94× at the highest tested load. Therefore the current design produces proofs after the fact, not making users wait online.

From Usable Prototype Toward Infrastructure

The current version proves the specified computation of an integer-quantized model under greedy decoding or fixed-seed sampling; it does not directly cover arbitrary floating-point services or sampling outcomes. Post-hoc proofs can detect tampering but cannot prevent an incorrect answer from reaching the user first. The zero-knowledge property for batched proofs has not yet been fully formalized in Lean. These boundaries chart the roadmap: compress proofs, reduce latency, complete formalization for batched scenarios, and establish equivalence between generated code and the Lean specification. FlashProve's value is advancing model-service trust one step forward: from trusting the provider's promise to verifying a single computation of the specified model.

Repository: https://github.com/anthropics/FlashProve Paper:

https://assets.claude.com/8e1d181a83015078581c92d896757041713f0160.pdf