Anthropic open-sources FlashProve, its provable inference prototype for MoE models
Anthropic’s Frontier Red Team, with collaborators at EPFL, MIT and StarkWare, built FlashProve, a prototype that produces a cryptographic proof that one specific language model generated one specific reply. The prover, two verifiers, the formal proofs behind them and a protocol specification are on GitHub under the Apache 2.0 license.
Source: Anthropic
When you send a prompt to a hosted API, you can’t confirm which model answered it. A provider could route the request to something cheaper, or someone with access to the inference server could tamper with the token stream, and the reply would still read like a competent reply. An outside evaluator faces the same problem in reverse, with no way to confirm that the model it tested is the model being served. FlashProve gives a checker a way to find out.
What’s in the repo
The repository holds three executables: the prover, a fast verifier written in C++, and a second verifier written in Lean, the proof assistant the team used to state and prove the protocol’s completeness, soundness and zero-knowledge properties.
The Lean verifier runs slowly, and that is fine, because its job is to be a reference. Lean establishes that this verifier accepts only the statements the soundness theorem covers, and on every test proof it agreed with the C++ verifier. The C++ one is for day-to-day use.
Anthropic says that the pieces might not line up. Three versions of this system exist: the paper, the Lean protocol, and the code that runs, and the team won’t promise all three say the same thing. Someone has to go through the Lean statements by hand to check, and the repo comes with an interactive visualizer to help. The prover has no formal tooling behind it, so that part gets audited the old way.
The weights aren’t in the release. FlashProve was tested on Llama 4 Maverick, a 400 billion parameter Mixture-of-Experts model (MoE), and you pull those weights from Hugging Face yourself under Meta’s license. One 80 GB GPU with about 290 GB of host memory is enough to run the prover, which only touches the roughly 17 billion parameters active per token and streams the weights through in layer-sized segments.
The numbers
On one H100 with 24 CPU cores, the prover moves about 110 tokens per second. A proof for a 1,024-token request runs about 18.78 MB, and checking it takes about 17 seconds on 24 CPU threads or about 21 seconds on a single thread. The offline step, where the prover commits to the weights, takes about 39 minutes once per model and then covers roughly 16 million requests. A client downloads a 6.5 MB commitment plus one proof per request. Measured against vLLM running the same model in FP8 on eight H100s, the overhead came to about 72 times per GPU across runs, and about 94 times at the heaviest load tested.
Download: The IT and security field guide to AI adoption
