Anthropic releases a provable-inference prototype and rests its trust on Lean statements a human can audit

The post describes FlashProve, a system that attaches a cryptographic proof to a model's response showing a specific model produced it. For Llama 4 Maverick (400B parameters, 4-bit weights), it reports about 110 tokens per second on one H100 and a proof of roughly 19 MB per 1,024-token request. That is about 70 to 95 times the GPU time of running the model on vLLM. The authors write that "Claude is good at optimization, but often makes decisions that are hard to evaluate", and respond by stating the security guarantees as top-level Lean statements. Code, Lean proofs and a spec are released under Apache 2.0, with a fast C++ verifier and a slower Lean one. The post lists its limits: a research prototype, contexts up to 1,024 tokens, proofs about an integer version of the model under greedy decoding, and no guarantee that the fast code matches the Lean protocol.

Why it matters: The stated method for agent-built code that is hard to review is to shrink what a person must check to a few formal statements and keep a slow, verifiable version beside the fast one. The authors say those statements still need a manual audit and the fast code is not covered, so the review gets smaller, not absent.