Anthropic Open-Sources FlashProve: Verifying the Authenticity of Model Outputs in 17 Seconds

Related topics top start Related topics top end Futures promotion begin Futures promotion end Miaopai begin Miaopai end Video player start Video player end Market chart begin Market chart end

You pay the price of a top-of-the-line flagship, you call the API of a resold router, and yet what is actually doing the work in the backend may be a shrunken small model.

This kind of "bait and switch" backroom operation was once the most secretive gray area in the entire large-model API supply chain.

With no weights and no data center, even if the backend is swapped out in the middle of the night and watered down to be less intelligent, developers can only stare helplessly and swallow the loss.

Today, this chain of backroom dealings has been cut clean through with a single stroke!

Just now, Anthropic, together with a founding-figure-level scholar of zero-knowledge proofs, announced a major breakthrough in "provable inference" for large models, officially open-sourcing the cryptographic verification system FlashProve!

From now on, developers need not trust any centralized institution, nor do service providers need to hand over a single line of weight code. Every time a large model generates an answer, it is forcibly stamped with a mathematical-grade "birth certificate."

Even with only an ordinary home CPU on hand, running for 17 seconds is enough to precisely verify, by purely mathematical means, whether every token was "born" from the target model, and any trick of swapping models or tampering midway will be exposed on the spot!

What is even more remarkable is that the core force behind building FlashProve this time was Claude itself.

When people usually feel that a large model has suddenly "gotten dumber," many will question the model with "who exactly are you," or throw a few math problems at it to probe.

But the model's own self-introduction is itself generated by the backend, and tiny fluctuations in compute load and sampling configuration can also change the answer, so users can never get ironclad evidence that would nail the service provider.

An even more chilling scenario was written into Anthropic's blog—

As models become stronger and capable of self-deployment, a more advanced model could very well take over the job of an approved weaker model, then disguise itself as the weaker model to evade the monitoring that should have been applied to it.

To verify authenticity, the traditional route is only to obtain the weights and rerun it yourself, but the weights of frontier models are each company's lifeline, and ordinary people simply cannot afford the data center needed for a 400-billion-parameter model.

To untie this dead knot without looking at the weights or rerunning the model, FlashProve split the verification process into three interlocking steps.

Step one, offline "fingerprinting."

Before the model goes online, the service provider spends about 39 minutes on a single H100 to generate a unique commitment ID for the model weights using zero-knowledge encoding and publishes it to the whole network. This string of IDs is like the digital DNA fingerprint of the weights; even secretly changing one parameter will make it fail to match, yet from the fingerprint alone outsiders can never reverse-engineer what the weights look like.

Step two, online "proof generation."

After each conversation request is processed, the service provider's GPU conveniently generates a cryptographic proof of about 19MB to confirm that this output was indeed computed by the model that was fingerprinted.

Step three, client-side "authenticity verification."

After any user or audit institution receives the answer, running the verification program cp_verify on an ordinary CPU takes 17 seconds to get a verdict of "true" or "false," with no weights and no GPU needed throughout.

The underlying engine supporting this magic is none other than zkSNARK (zero-knowledge succinct non-interactive argument of knowledge), famous in the cryptography world.

A verifier only needs to randomly spot-check a few places, like a teacher checking homework, to catch flaws with extremely high probability.

To break a single inference into a form that can be spot-checked, about 2,000 subprotocols called sumcheck must run behind each request.

Even more hardcore is that its security relies only on the hash function BLAKE2, not on algebraic structures such as elliptic curves, and it is even considered able to withstand future quantum computer attacks. This cryptographic route has also long been battle-tested in Ethereum Layer 2 networks such as Starknet.

With the principle explained, the real difficulty lies ahead: can such a heavy proof actually run on a 400-billion-parameter large model? article_adlist[

The team's test subject was Meta's Llama 4 Maverick, a 400-billion-parameter mixture-of-experts (MoE) model, with about 17 billion parameters actually activated per token.

FlashProve makes full use of this characteristic: when the prover generates the computation trace, its workload is proportional only to those 17 billion parameters that actually do the work, saving more than 95% of ineffective accompanying computation.

Even better, to prevent outsiders from reverse-engineering the secret of the model weights through "which experts were activated," the system uses zero-knowledge encoding to hide the routing choices in an indicator vector. When checking, the verifier performs a weighted sum over all experts, which both saves massive compute and keeps the model's internal operating path confidential.

After 4-bit quantization, the model weights are a full 232GB, while a single H100 has only 80GB of VRAM, so forcing it in would immediately blow out VRAM.

If the computation trace of the entire inference process were packed all at once, even the most luxurious graphics card could not bear it.

So the team put the weights in host memory, fed them into the GPU in segments, and completed computation and proof segment by segment.

When working, the H100 acts like an assembly line, each time streaming only one segment of weights from memory, and immediately after computing, completing encoding, hashing, and reduction in VRAM, retaining only a very small amount of data that needs to be passed to the next segment.

Through this kind of "eat one segment, digest one segment" streaming relay, a single 80GB graphics card managed to chew through a 232 GB behemoth.article_adlist[

At this point you are probably wondering how much effort from cryptography PhDs such a precise and intricate cryptographic protocol and GPU acceleration engineering actually consumed.

Open FlashProve's GitHub open-source homepage, and the language statistics bar on the right immediately exposes how unusual this project is.

In the entire repository, C++ code accounts for only 1.4%, Python 1.3%, and CUDA 0.9%, while a full 95.2% of the code (a full 398MB) is written entirely in the Lean 4 mathematical proof language.

Why would a large-model inference repository be stuffed with nearly 400MB of mathematical proofs? The 114-page protocol specification paper included with the repository gives the answer on page 51.

In this project, human scholars were only responsible for pointing out the direction. From this 114-page cryptography paper and 23-page technical report to the low-level C++ and CUDA code, and then to the nearly 400MB of Lean formal proofs, almost all of it came from Claude.

Not only writing code and papers, but every test, run, comparison, calculation, and code review in the project was also handled entirely by AI; wherever the text says "upon reading," "manually calculated," or "as reported," that reader, calculator, and reporter are all AI.

Cryptographic code has always been the most fragile forbidden zone in software engineering: even if a single symbol is written backwards or one random-number mask is missed, the entire security edifice collapses instantly.

Claude is very good at finding optimization paths in enormous systems, but the thousands of complex decisions it makes at the low level simply cannot be reviewed line by line by human experts with the naked eye.

Since humans cannot review it all, Anthropic simply brought in the mathematical world's iron-faced judge, Lean 4.

Here, every step of mathematical derivation written in must be checked line by line by the compiler kernel, and not a single mistake can pass.

Throughout the project, human scientists saved themselves the hard labor of reviewing hundreds of millions of lines of intermediate derivations, and only worked with the AI to finalize the 6 top-level security definitions, nailing three things down as iron laws.

Completeness. As long as the service provider honestly runs the model according to the promised weights, the generated proof will definitely pass verification, and the probability of being wrongly rejected is less than one in a trillion.

Knowledge soundness. If the service provider passes off a fake model or secretly changes a single token, the probability of the fraud slipping through is less than one in 2 to the 100th power, which is mathematically equivalent to impossible.

Zero knowledge. No matter how many times the client uses the proof for verification, the proof file will not leak the slightest bit of the model weights.

As long as these top-level theorems "say the right thing," then even if humans do not look at the nearly 400MB of tedious reductions in the middle even once, Lean 4's kernel has already guarded the gate for humans.

Even more interestingly, even the way this repository is opened has bid farewell to the traditional human programmer's manual.

The README states at the outset that it is "built specifically for Agents to run," and includes ready-made prompts and an AGENTS.md specification.

Looking back from a higher vantage point in time, the birth of FlashProve set off a profound technological convergence.

What it brings is a brand-new engineering paradigm: "AI builds the system, Lean guarantees truth and falsity."

Faced with a cryptographic engineering project of nearly 400MB of proof code and 114 pages of formula derivations, the reading limit of the carbon-based brain has already been breached.

In FlashProve, humans saved themselves the hard labor of reading line by line through C++ optimizations and tedious lemmas, and only held fast to the definitional authority over those 6 top-level theorems, letting AI climb the steepest cliffs of engineering and mathematics, and then letting the formal verifier act as the impartial gatekeeper.

Humans set the boundaries of the axioms, AI exhausts the maze of reasoning, and mathematics delivers the final judgment. This is precisely the hardest-core safety contract on humanity's path to superintelligence.article_adlist[

References:

Editors: Moses, Taozi ]article_adlistarticle_adlist[

]article_adlist news_keyword_pub,stock, iframe below the main text iframe below the main text general statement general statement QR code at the end start QR code at the end start

QR code at the end start QR code at the end start editor name and work code editor name and work code