Was the answer a chatbot just gave you really generated by the model it claims to be? With today's AI services, users have no way to verify this independently. If a provider quietly swaps in a cheaper model or tampers with the output, there is no way to detect it from the text of the response alone. Research into using cryptography to mathematically verify the results of AI computation is advancing to address this problem.
On November 2, 2026, an Anthropic research team released FlashProve, a system that uses zero-knowledge proofs (zkSNARKs) to verify the results of large language model (LLM) inference. The team demonstrated that it can generate proofs on a single NVIDIA H100 GPU for a 4-bit quantized version of Meta's Llama 4 Maverick (400 billion parameters, 128 experts). The result is not a peer-reviewed paper but a research prototype that includes AI-generated text and code, and detailed verification has not been completed. Even so, it is an important step: it offers concrete performance figures for verifying inference in large LLMs, which previously demanded enormous computing resources.
Proving Computation Results Without Revealing Model Weights
The "Provable Inference" approach FlashProve adopts lets a verifier confirm that a response matches the computation of a specified model, without obtaining the model's weights or rerunning the same computation. The weights of commercial AI models are normally not public, and even if they were available, ordinary users could not realistically run a model with hundreds of billions of parameters. Zero-knowledge proofs make it possible to prove that a computation was done correctly without revealing the model's internals.
FlashProve splits the process into offline and online stages. In the offline stage, the model provider creates a cryptographic "commitment" covering all of the weights. This is a cryptographic value that identifies the model's weights. It is published as roughly 6.24 MB of data, but the weights themselves cannot be recovered from it. In the online stage, the provider generates a proof of about 18.78 MB corresponding to the prompt and the response tokens, and the verifier checks it against the commitment to confirm that the computation was correct.
The design aims at four properties: "completeness," meaning a proof of a correct computation is accepted; "soundness," meaning forging a proof of an incorrect computation is computationally infeasible; "zero-knowledge," meaning the model's weights and intermediate computations are not revealed; and "succinctness," meaning proofs and verification stay small even for huge computations. Thanks to zero-knowledge, which experts a Mixture-of-Experts (MoE) model selected also remains hidden. The model's architecture itself, however, is not concealed. In addition, soundness depends on cryptographic computational-hardness assumptions and is not an unconditional mathematical guarantee.
Importantly, what is being verified here differs from ordinary LLM inference. FlashProve uses an integerized model built from publicly released 4-bit quantized weights, and it proves a deterministic computation based on greedy decoding, which selects the most probable token at each step. It cannot directly verify the floating-point arithmetic and probabilistic sampling used by typical AI services.
Exploiting MoE Sparsity to Generate Proofs on One GPU
Zero-knowledge proofs for large LLMs are difficult because they require far more computation and memory than ordinary inference. Converting a computation with hundreds of billions of parameters directly into a cryptographic circuit could exhaust memory even on a large GPU cluster. FlashProve addresses this by combining optimized cryptographic protocols with the structure of MoE models.
For its cryptographic foundation, it uses an interactive oracle proof (IOP). It combines techniques such as code proximity testing and lookup arguments, then converts the result into a non-interactive zkSNARK using a hash function. Because the construction relies on the security of the hash function, it is also expected to be quantum-resistant, but this is a theoretical property based on cryptographic assumptions and does not mean it has been demonstrated against quantum computers.
A key factor in reducing computation is the sparse structure of MoE. Llama 4 Maverick has 400 billion total parameters, but only about 17 billion are actually used in computing each token. FlashProve is designed so that proving effort scales with the computation of the actually activated parameters rather than the whole model. Expert selection information is also not disclosed to the verifier.
On the hardware side, the roughly 232 GB of quantized weights are held in about 290 GB of CPU-side memory rather than in GPU VRAM. By splitting the model layer by layer and transferring the needed weights in sequence to an H100 with 80 GB of VRAM, the system can handle a model larger than a single GPU's capacity.
FlashProve also adopts "post-hoc proving," which separates response generation from proof processing. After responses are generated, the computations of multiple requests are processed together, sharing weight loading and commitment-related work to improve efficiency. This avoids delaying the delivery of responses for proving, but issuing a proof involves a separate waiting time and requires redoing the computation. The current implementation is optimized for MoE models and does not support distributing proof processing across multiple GPUs.
110 Tokens per Second, but About 72 Times the Compute of Standard Inference
The research team evaluated the 4-bit integerized Llama 4 Maverick on a single H100 GPU and 24 CPU cores. The security parameter targeted 128-bit security, and the offline processing at model onboarding took about 39 minutes. According to the report, the commitment created in this step can be reused to verify about 16 million requests.
For online proving, the system processed 24 requests in a batch, each with a 1,024-token context, and generated proofs in about 223 seconds. Dividing total processed tokens by elapsed time gives a throughput of 110 tokens per second.
This figure does not mean the system can generate and prove 110 new response tokens per second, however. It is a processing speed that includes the entire 1,024-token input context, and under the standard measurement conditions only the final token of each request is actually proven. When every token was made a proving target, the verified-token throughput was 39.1 tokens per second.
| Condition | Result | Notes |
|---|---|---|
| Batch proof of 24 requests | About 223 seconds, 110 tokens/s | Speed over the full context; only the final token is proven |
| Single-request proof | 58 seconds, 17.6 tokens/s | Processes a 1,024-token context |
| All-token verification | 39.1 tokens/s | Every token in the context is proven |
| Proof verification on CPU | 17 seconds (24 threads), 21 seconds (1 thread) | No GPU required |
| Proof size | About 18.78 MB/request | Commitment-related data is about 6.24 MB |
| GPU time vs. standard inference | About 72x (66–77x) | Compared with FP8 inference on vLLM |
Batching improved processing efficiency, but issuing a proof still takes about 223 seconds. A verifier who receives a proof, on the other hand, can complete verification in 17 to 21 seconds using only a CPU, with no GPU. Most of the computational load is concentrated on the proof-generation side, keeping verification lightweight.
The team also compared it with vLLM, an inference engine running the FP8 version of Llama 4 Maverick on eight H100s. Converted to per-GPU processing time, FlashProve's proof generation required about 72 times (66 to 77 times) the GPU time of standard inference, and the gap reached about 94 times against vLLM running at maximum load. However, the comparison targets differ in numerical format and execution configuration, and the absolute GPU times used to calculate the ratios cannot be confirmed from the published materials, so this is not a simple like-for-like comparison.
Considering that the earlier work VerInf needed about 14.3 hours to prove 1,000 tokens for the same model and produced a proof of about 93.6 GB, FlashProve substantially reduces both processing time and data volume. Even so, the computational load remains large compared with standard inference. These performance figures are the research team's own measurements, and independent third-party replication has not been completed.
Formal Verification in Lean, and Remaining Implementation Safety Issues
To confirm the correctness of its cryptographic protocol, FlashProve uses the Lean theorem prover. Under the random oracle model, the team formally proved the main properties of completeness, soundness, and zero-knowledge. However, a mathematical protocol being verified is not the same as the safety of the entire running software being proven.
The released code includes a Lean verifier that corresponds directly to the theorems and a C++ verifier that runs at practical speeds. The two return the same judgments in tests, but proving their mathematical equivalence remains a task for the future. In addition, the fast prover implemented in CUDA and C++ includes AI-generated code, and there is no guarantee that it fully matches the Lean specification.
Implementation defects can cause proofs of correct computations to fail, and if zero-knowledge is compromised, there is also a risk that information such as model weights could leak. If the verifier is correct, soundness, meaning invalid proofs are not accepted, is maintained, but this does not guarantee the safety of the prover. Furthermore, at the time of release, the complete formal Lean proof of zero-knowledge was finished only for individual-request proofs, and parts of batch proofs remain unresolved.
Formal verification has other boundaries as well. Whether a specification written in Lean accurately captures the security requirements actually needed requires human scrutiny, and trust in the execution environment and compiler is also assumed. In addition, the scope of the guarantee differs between verifying exact matches and "clipped-gap acceptance," which tolerates error. The latter guarantees results only within a configured tolerance and does not prove that arbitrary computation results match exactly.
Applications: Preventing Model Substitution and Third-Party Audits
If FlashProve is put to practical use, it could become a means of increasing the transparency of AI services. For example, it could be used to check that an intermediary has not secretly swapped a specified model for a cheaper one, or to support independent model evaluation by external assessment bodies. Other envisioned uses include proving that security scans or business analyses were run on a specified model, and giving regulators a way to confirm that an approved model is in use.
The research team also proposes applying it to "pacing," the management of the pace of AI development. Requiring providers to submit inference proofs periodically would make it possible to confirm that inference with the designated model was actually performed. However, it cannot prove that model training was not being carried out in parallel on the same computing facilities.
The security limitations are also clear. Post-hoc proving is a mechanism for discovering invalid computation or tampering after the fact; it does not prevent incorrect answers or malicious output from reaching users in real time. Conventional measures such as secure boot, isolated execution environments, and audit logs are still needed to prevent theft of model weights and similar threats.
Above all, what can be cryptographically proven is that "the specified model produced this computation result," not that "the content of the answer is correct." Even a response containing factual errors or harmful content will pass proof if the model computed it correctly.
For practical use, support is needed for the floating-point arithmetic and probabilistic sampling used in typical AI services. The integer-quantized model used here and real floating-point inference show empirically similar results on ordinary prompts, but a match is not guaranteed against adversarial prompts designed to induce differences. Other challenges include the verifiable context length being limited to 1,024 tokens, and side-channel attacks that infer internal information from proof-generation time being outside the scope of the defenses.
FlashProve is not a feature introduced into Anthropic's commercial AI service Claude; it is a research prototype released under the Apache 2.0 license. The result shows that cryptographic inference verification is possible even for LLMs with hundreds of billions of parameters, through post-hoc batch processing taking on the order of minutes. Challenges remain, however, in the heavy computational load relative to standard inference, the safety of the implementation, and numerical compatibility with real AI services. The focus going forward will be on closing the gap between formally verified theory and fast execution code, and on how efficiently verification can be done in actual operation.
