A cryptographic proof to verify which AI model actually responded

With FlashProve, Anthropic explores a method to certify the origin of an AI’s responses without revealing its parameters, thanks to cryptographic proofs.

Nothing currently guarantees to a user that the artificial intelligence model they believe they are addressing is indeed the one producing the response. An intermediary could substitute a cheaper model, a compromised server could alter the results, and even an independent auditor might not necessarily have the means to verify the identity of the system used. This difficulty takes on another dimension as models become involved in sensitive operations, from cybersecurity to the assessment of systems subject to regulatory obligations.

A research team from Anthropic, working with specialists from EPFL, MIT, and Succinct, has developed FlashProve, a prototype capable of producing a cryptographic proof linking a response to the parameters of a specific model. Presented in a publication dedicated to verifiable inference, this system uses zero-knowledge proofs, known as zkSNARKs, to establish that a computation was performed correctly without exposing the confidential information used to carry it out. Proving the origin of a response without accessing the model

FlashProve works in two stages. Before any request, the provider publishes a cryptographic commitment, a kind of fingerprint associated with a specific set of model parameters. These parameters remain secret, but the commitment serves as a reference for verifying responses produced later.

When a request is submitted, the provider can generate a certificate demonstrating that the verified tokens correspond to the output of the model associated with that fingerprint. The user, or a third-party auditor, then checks the validity of the proof without downloading the parameters or running the model themselves. Verification therefore requires far fewer resources than the initial computation.

This method does not certify that a response is true, relevant, or free from bias. It establishes a different property: the verified elements do indeed come from a defined computation, performed with the parameters to which the provider committed. This distinction is important for services that offer multiple models behind a single interface, but also for companies wishing to attest that an analysis was actually performed by a given system. A 400-billion-parameter model verified on a single H100

The researchers tested their system on Llama 4 Maverick, a 400-billion-parameter mixture-of-experts model, of which around 17 billion are mobilized for each token. The tests use a four-bit quantized version and a proof system involving a single NVIDIA H100 card, accompanied by 24 CPU cores.

In this configuration, FlashProve processes around 110 context tokens per second when generating proofs, on a batch of 24 requests. Each one covers a window of 1,024 tokens, and the proof verifies a single token selected per request. The figure of 110 tokens per second therefore does not correspond to verified text generation at that rate.

Each certificate is about 18.78 MB. Verification takes 17 seconds with 24 CPU threads, or 21 seconds on a single thread, without requiring a graphics card. The initial preparation of the cryptographic commitment takes about 39 minutes, but that operation can then be used for about 16 million requests before being renewed.

The computing cost remains significant, however. According to the measurements detailed by Anthropic, generating the proofs uses between 70 and 95 times more GPU time than the reference execution with vLLM, depending on the tested workload. The comparison is based on different hardware and numerical configurations and does not constitute a universal multiplier applicable to all models. Mathematical guarantees examined with Lean

An additional difficulty arises when it is necessary to verify the system responsible for producing and checking these certificates. An error in its implementation could weaken the security guarantees, even if the cryptographic principle itself is sound.

To limit this risk, the researchers used Lean, a formal proof assistant that makes it possible to represent mathematical properties and verify their proof. Three main guarantees are examined: acceptance of honest proofs, rejection of fraudulent proofs except with negligible probability, and the absence of disclosure of secret parameters through the certificate.

The project includes a fast verifier written in C++ and a second implementation in Lean, slower but linked to the formally proven properties. This separation makes it easier to examine the mathematical foundations while retaining a tool that is usable for experiments.

It does not, however, eliminate all risks. The researchers acknowledge that the correspondence between the formalized properties, the documentation, and the entirety of the executable code is not itself entirely guaranteed. The system protects the model parameters, but not its architecture, and some information could theoretically be revealed by indirect channels, such as observing computation times. A path toward controlling providers and authorized models

Verifiable inference could address several problems encountered by organizations that use external models. A client going through a routing service would be able to verify that they are indeed receiving the responses of the intended model, while an independent evaluator could check that the system being tested corresponds to what is actually offered to users.

The envisioned applications also concern monitoring the most advanced models. An authority could require proofs showing that only certain authorized versions are being used, without having access to their confidential parameters. These certificates could also help track providers’ inference activity, even if they would not be enough to establish that their infrastructure is not simultaneously carrying out other operations, such as training.

This prospect remains constrained by several technical limitations. FlashProve currently works on an integer representation of the model with deterministic decoding, which does not directly cover all