Analysis
Proof sounds like a guarantee. Anthropic's FlashProve is narrower than that. The research page, dated November 2, offers code, a protocol specification and Lean artifacts for proving inference against committed model weights, and calls the release a research prototype.
Here is the hinge. A proof about committed weights is not a production claim. The page makes no claim of deployment on Claude.
The reported evaluation is narrow and costly. It uses an integer, greedy-decoded version of Llama 4 Maverick, with contexts up to 1,024 tokens. Proof generation is reported at roughly 70 to 95 times ordinary inference GPU time.
One gap stays open. The authors do not guarantee equivalence among the Lean protocol, the paper and the fast executable code.
Three questions to hand to anyone pitching this. Which committed weights would a proof name? Do the protocol, the paper and the fast code agree? Which jobs could carry a bill of 70 to 95 times the GPU time?
Source: Progress on provable inference for large language models · 2026-11-02 · Primary source context · attributed account
Why it matters
A proof sounds like assurance for a live service. The page supports something smaller: a prototype, a capped test and an unresolved match between code and spec.