How Fast Can FlashProve Go?

§1.Introduction

Note: This post assumes you are familiar with the content of ZK-SNARKs from the Ground Up. General ZKP knowledge should suffice, though I will use my preferred terminology and notation, which might differ a bit from conventions in the literature.

Anthropic’s FlashProve is a state of the art ZK-SNARK for LLM inference, developed almost entirely by Claude.¹¹With some help from Giacomo Fenzi, Guy Weissenberg, Miranda Christ, Rahul Dalal, Alessandro Chiesa, Roy Rinberg, Alex Allain, and yours truly!⁠ FlashProve is fast, capable of achieving ~100 tokens per second on a single H100 when proving Llama 4 Maverick, and is orders of magnitude faster than prior open source work. FlashProve is faster because of changes at both the protocol level (e.g. the ZOOK hiding scheme, batching across many proofs), and the implementation level (efficient kernels).

I’ve said publicly that I believe there’s still lots of speedups on the table. I see this coming from both protocol and implementation improvements. On the protocol level, I expect models to accelerate research on the mathematical foundations underlying SNARK protocols²²Like via smaller proximity gaps and ways of using structure from different branches of math to accelerate SNARKs.⁠, and to be able to eke out gains from further specialization of the building blocks involved to inference. With respect to implementation, we can already see how, with each generation, models get better and better at optimizing kernels and hillclimbing throughput benchmarks. To forecast future progress in provable inference, I think it’s worth looking at how much progress we can expect to get from implementation alone, as unlike with protocol progress, it’s possible to get a rough estimate of the upper bounds on speedups of the current approach.³³For what it’s worth, SNARKs with asymptotically linear time provers already exist, so the real question is what constant factor we can get down to, which is much harder to answer.⁠

§2.Background

I first want to go over the “gist” of how FlashProve works, so we can refer to these pieces in our analysis. Recall that we’re proving Llama 4 Maverick, which looks like so:

Figure 1: The architecture of Llama 4 Maverick (400B).

Every layer does standard GQA attention on the residual followed by a feed forward block, each with a norm (RMSNorm) in front of it and a residual connection around it. The layers alternate between having a dense (single MLP) and sparse (128 expert MoE) feed forward block, but are otherwise identical. For the sake of compactness I’ve drawn attention and norms as single blocks, but of course we’ll ultimately prove them by breaking them down into their constituent operations (QKV projections, softmax, etc).

However, FlashProve doesn’t prove “normal” Llama 4 Maverick. It proves an integer quantized version, using fixed point arithmetic. This means that every product has to be rescaled afterwards, and many of the results get clamped too⁴⁴See Wikipedia for why/how if you are unfamiliar with fixed point arithmetic.⁠, both of which are non-polynomial operations. As we will see shortly, these are very much not free.

Let’s zoom in on the dense layers, as they are simpler, and look at a version with all the fixed point machinery included:

Figure 2: One dense layer of the integer model.

Okay, so how are we going to prove that given some input residual x, and the committed weights, that we’ve produced a correct output residual x′′? At a high level, we’ll use the sum-check machinery from ZK-SNARKs from the Ground Up, though not quite GKR: rather than working backwards from the output one layer at a time, the prover commits to nearly every intermediate value as it goes, and sum-check reduces each polynomial operation to claims about those committed values and the weights, which we can verify via openings. For non-polynomial operations, such as the SiLU, norms, clamps, etc, we’ll have to commit to their outputs and use lookups to prove they’re correct.

Below is a version of our diagram updated to show which operations will be proved via sum-check () and which will require lookups (). All the sum-checks and lookups will bottom out in linear claims about committed tables.⁵⁵Checks in the protocol (like a lookup checking that its two products are equal) become claims about committed tables too, due to the hiding scheme (ZOOK).⁠

Figure 3: The dense layer of Figure 2, with the values the prover commits to in blue and the ones it never commits to in gray.

Note: MoE layers are identical, except we have to prove the routing computation and the choice of expert (each token goes to one of the 128 routed experts, plus a shared expert every token uses), and then run those MLPs. There’s some additional complexity for the output head and embeddings step of the model, but we’ll ignore those here.

The model is split into segments. For each segment, the prover commits to the segment’s intermediate values, and then runs the corresponding sum-checks and lookups. The sum-checks and lookups leave claims about the committed intermediate values and, of course, the weights. Each segment’s commitment only gets the first step of a recursive opening: a few of its columns are opened, but its folded row (the weighted sum of all its rows that an opening would normally send, G_(r_(row)) in Ground Up) isn’t sent. It’s only checked with arithmetic, so it’s committed as part of the next segment’s commitment instead. The claims roll forward like this from segment to segment, until all of a request’s intermediate values are settled by a single full opening at the end. Claims about the weights are all merged into one claim about the weight table that’s also settled via opening at the end of the request, but batched with other requests (more on this in Section 2.1).

Figure 4: One request’s chain of segments. Each folded row is committed into the next segment, and the weight claims are merged into one claim that’s opened once per batch.

To make the proof non-interactive, Fiat-Shamir is used (as is standard). Every challenge is a hash (BLAKE2b) of everything the prover has sent so far. As a defense against grinding, the protocol also requires a proof of work (28 bits for the weights, 20 bits for intermediate values) before every challenge that picks which columns to open, since otherwise those challenges fall short of 128 bits of security.

Weights are committed as two signed bytes each, then the codewords are arranged into one giant 2048 row, 2^(32) column matrix. There’s a one time range proof step, which we’ll skip explaining in detail here.

In ZK-SNARKs from the Ground Up, we required commitments to be δ-close for δ < (1 − ρ)/2, so that each one could only be close to a single table. FlashProve allows a much bigger δ (up to the Johnson radius), so each opened column is more likely to catch a cheater and far fewer need to be opened.⁶⁶Recall that each opened column catches a δ-far commitment with probability more than δ.⁠ The catch is that a commitment can then be close to several different tables at once, so right after each commitment, the verifier picks a random point (an OOD sample) and has the prover say what the table’s extension is there. Different tables almost never agree at a random point, so this pins the commitment down to just one of them.

§2.1.Batching

The opening of the weight commitment is one of the most expensive parts of the proof, but this cost can be amortized via batching. Batches of requests are run side by side, and then their weight claims are merged into a single opening which validates all of them.⁷⁷Claims each requests’ segments’ committed intermediate values are still resolved via individual openings.⁠

At the end of a request’s chain of segments, we’re left with one claim about a weighted sum of the weight table. Rather than opening the weights for every request, the prover does the first step of a recursive opening, committing to the weight table’s folded row (Claude calls this a request vector) instead of sending it, but holds off on checking it. Once every request in the batch has committed its request vector,⁸⁸So none of them can change it after seeing the shared point.⁠ the verifier picks a single random point shared by all of them, the weight table gets one real opening there, and each request vector is checked against it.⁹⁹Why not just merge the claims as usual? Then every proof would have to include every request’s claims, leaking other users’ prompts and making each proof up to 64x bigger. This way, each proof only depends on the others through a hash.⁠ Every batch does exactly one opening of the weight table, which involves checking 64 columns of the weight table, no matter how many requests it holds.

Figure 5: A batch of requests sharing a single opening of the weight table. Each request commits to its request vector, a hash of all of them gives the random point, and each request vector is checked against the one opening.

§3.Rooflines

Let’s start by establishing the coarsest, but highest confidence upper bounds. We can do this by figuring out which operations which have a well-defined hardware upper bound the protocol forces us to do, and then measuring how fast our hardware (H100 GPUs) can do them.

To get a feel for this, say we didn’t want to prove anything, and just wanted to run Llama 4 Maverick. It’s a sparse MoE model, so each token only uses about 17B of its 400B parameters, and each parameter costs one multiply and one add. So a token takes about 2 × 17 × 10^9 FLOPs.¹⁰¹⁰Attention adds a bit on top of this, but with 1,024 tokens per request it’s only about 0.5 GFLOPs per token.⁠ An H100 can do at most 989 TFLOPS (989 × 10^(12) FLOPS) of dense BF16 matmuls, so it can’t run the model faster than:

(989 × 10^(12) FLOP/s)/(34 × 10^9 FLOP/token) ≈ 29,000 tokens/s.

Note that this ignores memory and bandwidth considerations entirely,¹¹¹¹The 800 GB of BF16 weights don’t even fit on one H100!⁠ but that’s the point of a roofline: we can’t do better than the best upper bound from any of our resources!

FlashProve does ~100 tokens per second today, far below this, so the model’s inherent FLOPs are clearly not what’s holding it back.¹²¹²These run on the tensor cores anyway, which are otherwise mostly idle, so they can largely overlap with everything else.⁠ So what should we count instead? We want work that the protocol forces, that’s easy to count from the model’s shapes, and that has a clear performance upper-bound on our hardware.

§3.1.Committing intermediate values

Recall that the prover commits to most intermediate values: the rounded and clamped values, the outputs of SiLUs and norms, the digits it uses to prove values are small, etc (the blue tables in Figure 3). Committing to a table means Reed-Solomon encoding each row (an NTT¹³¹³Number Theoretic Transform, basically a DFT over a finite field. See Wikipedia if you’re unfamiliar.⁠) and Merkle hashing each column (using BLAKE2b), which are both standard operations with well-understood costs.

How much intermediate data do we actually commit to? Looking back at Figure 3, the prover commits to every value in blue, but that’s not quite everything. Take the gate’s rescale, g_w = ⌊ĝ ÷ 2^(k_g)⌉. The prover never commits to ĝ, so to prove the rescale it also commits to the remainder, the low bits that got rounded away, r_g = ĝ − 2^(k_g) g_w. Now the matmul’s sum-check can use 2^(k_g) g_w + r_g in place of ĝ, and a lookup checks that r_g is small (i.e. that the rounding was honest). Every rescale works like this, so each one adds a committed remainder. If that went too fast for you, don’t worry, it doesn’t really matter. The only thing you need to take away is that every rescale introduces a couple values that need to be committed (which I neglected to show in Figure 3).

Figure 6: The prover commits to g_w and the remainder r_g instead of ĝ. The matmul’s sum-check uses 2^(k_g) g_w + r_g in place of ĝ, and a lookup checks that r_g is small.

FlashProve also splits every value into 8-bit limbs (so a 16-bit value is two limbs), and packs three limbs into each field element.

Figure 7: Two 16-bit values split into four 8-bit limbs. Each limb sits at the bottom of its own 20-bit slot, so three fit in a 64-bit field element and the fourth starts the next one.

Why? Doesn’t FlashProve use the Goldilocks field (2^(64) − 2^(32) + 1), meaning we have capacity to pack up to 7 limbs per field element?

The catch is how FlashProve proves that limbs are small. Rather than checking every limb with a lookup, it checks a few random combinations of them, which is much cheaper, but only shows each limb is below about 2^(18), not 2^8. So each limb gets a 20-bit slot, which makes sure a field element can only be unpacked one way, and three 20-bit slots fit in 64 bits but four don’t.

Let’s now do an accounting of one dense layer of one request (1024 tokens):

g_w, g_k, s and u, the MLP’s hidden values, each a [1024, 16384] matrix of 16-bit values (2 limbs each).¹⁴¹⁴The gate shows up three times (g_w, g_k, s) because the clamp and the SiLU are both proved by lookups, so each of their outputs has to be committed. The gated product h is just a product, so sum-check handles it without committing to it.⁠ ⁠ Adding the 1-limb remainders r_g and r_u, that’s 4 × 2 + 2 = 10 limbs per hidden unit, or 10 × 16384 × 1024 ≈ 1.7 × 10^8 limbs.
⁠The attention scores, a [1024, 1024] matrix for each of the 40 heads. Only the causal half is needed, but it’s computed in 128 × 128 tiles, so it pads out to 576 keys per query on average. At 5 limbs per score, that’s 5 × 40 × 576 × 1024 ≈ 1.2 × 10^8 limbs.
⁠x′, x′′, a_w, a, m_w and m, the residual stream and the norms, each a [1024, 5120] matrix. Along with their remainders, that’s about 23 limbs per entry (the residual stream alone takes 5), or 23 × 5120 × 1024 ≈ 1.2 × 10^8 limbs.
The queries, keys, values and attention’s output, before and after their rescales, another 0.6 × 10^8 limbs.

That’s about 4.7 × 10^8 limbs per layer.¹⁵¹⁵MoE layers commit about the same, since a token’s shared and routed experts are together as wide as the dense MLP.⁠ Multiplying by the 48 layers and adding the output head’s logits (6 limbs for each of the 202,048 vocabulary entries, per token), we commit to about 2.4 × 10^(10) limbs per request. The digits for proving all of these are small, plus some bookkeeping, bring it to about 3.5 × 10^(10). Packed three to a field element, that’s 2,790 rows of 2^(22) elements per request, and at 8 bytes per element, about 90 MB per token, or 6 TB for a batch of 64 requests.

For the batch:

Encoding. Each row of 2^(22) elements is encoded into 2^(23) elements with an NTT of 22 × 2^(22) butterflies, so 2,790 × 64 × 22 × 2^(22) ≈ 1.6 × 10^(13) butterflies in total. A butterfly is about 15 integer instructions,¹⁶¹⁶It’s one field multiplication and two field additions, and most of the multiplications are by powers of two, so they become shifts.⁠ so an H100 does about 1.1 × 10^(12) per second, which takes 15.5 s.
Hashing. Every column of every encoded table becomes a salted Merkle leaf, and the leaves are hashed up into a tree. That’s about 1.8 × 10^(11) BLAKE2b compressions per batch. Password crackers have optimized BLAKE2b on GPUs for years, and hashcat does about 7.2 billion per second on an H100 PCIe. Scaled up to the H100 SXM, that’s about 8.4 × 10^9 per second, which takes 21.9 s.
Everything else. Generating the salts, the proofs of work, and the smaller commitments (e.g. to the request vectors) add another 3.7 s:
- Salts. The salts (and the random masks that hide the tables) take about 5.2 × 10^(10) ChaCha20 blocks. A block is about 1,100 instructions, so an H100 makes about 3 × 10^(10) per second, which takes 1.75 s.
- Proofs of work. Each batch grinds 10 proofs of work of 28 bits for the weight opening, and each request grinds 36 of 20 bits, so that’s 10 × 2^(28) + 64 × 36 × 2^(20) ≈ 5.1 × 10^9 BLAKE2b hashes, which takes 0.6 s.
- Smaller commitments. Values that get re-sent to later segments, the request vectors and the other small tables add about 9.5 × 10^(11) butterflies and 3.9 × 10^9 compressions, which take 0.9 s and 0.5 s.

Figure 8: Committing to one request’s table. Each row is encoded to twice its length, then each column (with a salt) is hashed into a leaf, and the leaves are hashed up into a single root.

Putting it together:

(64 × 1,024 tokens)/((15.5 + 21.9 + 3.7) s) ≈ 1,600 tokens/s.

So with perfect kernels, FlashProve can go at most ~13x faster than it does today before the commitments alone become a hard bottleneck.¹⁷¹⁷Spreading the batch over an 8 GPU node doesn’t help per GPU, as all of this work just splits eight ways.⁠ Note that while this tells us we can’t go any faster than 1600 tok/s, it’s not a tight upper bound. There could be (and as we’ll see, are) other bottlenecks that bring it down further.

§4.Tighter Rooflines

Let’s now go a bit beyond simple rooflines, and try to do some accounting of the actual operations involved at every step the prover takes.

There aren’t good public benchmarks for most of these operations, so here we’ll count instructions instead. An H100 can issue at most about 3.3 × 10^(13) 32-bit integer instructions per second.¹⁸¹⁸132 SMs, each issuing 128 per clock (64 on the integer pipe and 64 multiply-adds on the FP32 pipe), at 1.98 GHz.⁠ We’ll also switch to an 8 GPU node, with the batch spread across all eight GPUs, and add up time per batch in GPU-seconds, so the tokens per second come out per GPU.

Commitments. From above, 41.1 s.
Lookups. A lookup shows that its keys are all rows of a table by showing that two products are equal, one over the keys and one over the table. The product over the keys is built up as a binary tree, and each level of the tree is proved with sum-check. There’s a key for every rounded, clamped or nonlinear value, plus the digits for proving values are small, about 1.6 × 10^(10) per request. Each key costs about 3.5 multiplications in the extension field,¹⁹¹⁹A plain product tree costs about 7 per key: about 1 to build it, and about 6 for the sum-checks that prove it. But the keys are small integers, so most of the tree’s multiplications are by small numbers, which are about 4x cheaper. Turning values into keys adds about 0.75 more.⁠ and each of those is about 140 instructions,²⁰²⁰Goldilocks elements are 64 bits, so multiplying two of them takes several 32-bit multiplications, and the extension field multiplies several of those together.⁠ so an H100 does about 2.4 × 10^(11) per second. That’s 64 × 1.6 × 10^(10) × 3.5 ≈ 3.7 × 10^(12) multiplications per batch, which takes 15.5 s.
Decoding weights. The prover stores the weights compressed (in llama.cpp’s quantized formats), so they have to be decoded before they can be used. Each request decodes all 400B weights three times: once to run the model, once for the matmuls’ sum-checks, and once to merge the weight claims into one.²¹²¹The decoded weights take 800 GB, so they can’t be kept around between passes.⁠ That’s 3 × 64 × 4 × 10^(11) ≈ 7.7 × 10^(13) decodes per batch, at about 3 instructions each, which takes 7.2 s.
Everything else. The rest of the sum-check work, the openings, and the integer work of running the model add another 4.6 s.

Figure 9: A lookup checks that two products are equal. Each key k becomes α − k for a random α, and a tree multiplies them in pairs up to one product, with each level proved by sum-check. On the table side, each row is raised to the number of times it was looked up.

Putting it together:

(64 × 1,024 tokens)/((41.1 + 15.5 + 7.2 + 4.6) s) ≈ 960 tokens/s per GPU.

§5.Conclusion

We found that, without protocol changes, FlashProve can be sped up by at most ~8x, to about 960 tokens per second per H100. This is significant, but not groundbreaking. What prover speeds are sufficient depends on the use case. For treaty verification, even FlashProve’s current overheads might be sufficient, as only random sample proofs may be required. For preventing token output streams from being compromised, protocol changes are required before overhead is low enough such that this is commercially viable.

TODO: concluding sentence