How Fast Can FlashProve Go?

Tldr: I estimate that, without protocol changes, FlashProve’s throughput is capped at around 2,800 tokens per second per H100, barring a BLAKE2b¹¹The hash function used for FlashProve’s commitments. kernel substantially faster than hashcat’s. This is the tightest upper bound I find defensible, but the true limit is likely much lower. You may find this analysis interesting if you want to understand more about how FlashProve works under the hood, or just enjoy performance modeling.

§1.Introduction #

FlashProve is a state of the art ZK-SNARK for LLM inference.²²Built by Giacomo Fenzi, Guy Weissenberg, Miranda Christ, Rahul Dalal, Alessandro Chiesa, Roy Rinberg, Alex Allain, yours truly, and of course, Claude. The views and estimates (and any mistakes) in this post are my own. FlashProve is fast, capable of achieving ~123 prefill tokens per second per H100 when proving Llama 4 Maverick,³³At 64 requests per batch. More benchmarks here. and is orders of magnitude faster than prior open source work. FlashProve gets its speed from improvements 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 are still lots of speedups on the table. I see these coming from both protocol and implementation improvements. On the protocol level, I expect LLMs to accelerate research on the mathematical foundations underlying SNARK protocols⁴⁴E.g. via stronger proximity gap results, and ways of using structure from different branches of math to accelerate SNARKs., and to be able to eke out gains by further specializing the protocol’s building blocks to inference. With respect to implementation, we can already see how, with each generation, LLMs get better and better at optimizing kernels and hill-climbing throughput benchmarks.

An interesting question then, is how much progress we could get from implementation improvements alone. If there’s lots of headroom, we may not have to invest much in protocol research, but if we’re already close to the ceiling, that’s a strong sign we should be working on better protocols instead of trying to squeeze more out of the current one.⁵⁵Note that I’m counting parameter changes (e.g. trading off proof size for speed) as protocol changes. In this post, I’ll take a stab at upper-bounding the performance of the FlashProve protocol in tokens per second per H100, assuming the protocol is fixed, and that the best known algorithms for its building blocks (like NTTs and hash functions) are as good as it gets.⁶⁶Given the state of TCS lately, this may not be as safe an assumption as it seems, but without this it’s pretty hard to reason about upper bounds at all…

Note: I’ll assume you’re familiar with my earlier post, ZK-SNARKs from the Ground Up. General SNARK knowledge should suffice, though I’ll use my preferred terminology and notation, which might differ a bit from conventions in the literature.

§2.Background #

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

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:

Okay, so how are we going to prove that given some input residual x, and the committed weights, 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. Instead of 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.

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 mostly 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 couple hundred 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. The verifier would only ever use the folded row in two weighted sums (folding it to the claimed value, and comparing its encoding with the opened columns), so instead the prover commits to it as part of the next segment’s commitment, before the columns to open are picked, and those two checks become claims about that commitment. The claims roll forward like this from segment to segment, until all of a request’s intermediate values are checked 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 checked via an opening at the end of the request, but batched with other requests (more on this in Section 2.1).

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. To make it expensive for a cheater to retry for a luckier challenge, 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 (four for the embedding), then the codewords are arranged into one giant 2048 row, 2^(32) column matrix. There’s a one time range proof step that checks all the weights’ values are in their expected ranges (each byte in [−128, 127] and each weight in [−4096, 4095]), 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 bigger δ (up to the Johnson bound). This means each opened column is more likely to catch a cheater, so fewer of them need to be opened.⁹⁹Recall that each opened column catches a δ-far commitment with probability more than δ. But now a commitment can be close to several different tables at once (this is called the list decoding regime), so how do we know which one the prover committed to? To fix this, the verifier picks a random point (an OOD sample) right after each commitment, and has the prover say what the table’s extension is there. Since different tables almost never agree at a random point, this pins the commitment down to just one of them with high probability.

§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 share a single opening which validates all of them.¹⁰¹⁰Claims about each request’s segments’ committed intermediate values are still resolved via individual openings.

At the end of a request’s segment chain, we have a claim about a weighted sum of the weight table. Instead of opening the weights to check this claim, the prover commits to a partial fold of the weights (Claude calls this a request vector), and we hold off on checking it for now. 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 one random point shared by all requests. The weight table gets one real opening at that point, and each request vector is checked against it.¹²¹²Why not just merge all the weight claims into one? Then each user’s proof would have to contain every other request’s claims, which would leak other users’ prompts and make each proof grow with the batch size. With request vectors, proofs in a batch only depend on each other through a hash. So there’s only one opening of the weight table per batch, of 64 columns, regardless of the number of requests.

§3.Analysis #

Now that we’ve covered how FlashProve works at a high level, let’s think about how we can upper-bound its performance. We can do this by figuring out which operations 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:

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 ~123 tokens per second today, way below the ~29,000 bound above, so the model’s FLOPs aren’t the bottleneck.¹⁵¹⁵Those run on the tensor cores, which are otherwise mostly idle anyway, so they can largely overlap with everything else. So what do we count instead? Well, we want to count work the protocol forces us to do, that’s easy to count from the model’s shapes, and that has a (relatively) clear hardware upper bound.

Let’s look at the commitments. 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.) and Merkle hashing each column (using BLAKE2b), which are both standard, well-studied operations, so we can make a reasonable estimate of how fast an H100 can do them.

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 = ⌊ĝ ÷ 2^(k_g)⌉. The prover never commits to ĝ, so to prove the rescale it also commits to the remainder, the part that got rounded away, r_g = ĝ − 2^(k_g) g_w. Now the matmul’s sum-check can use 2^(k_g) g_w + r_g in place of ĝ, 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 didn’t make a lot of sense, 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).

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.

Why? Doesn’t FlashProve use the Goldilocks field (2^(64) − 2^(32) + 1), meaning we have room to pack up to 7 limbs per field element? In theory, yes, but padding this way enables a trick FlashProve uses to cheaply check that every limb is small, which would otherwise take a lot of lookups.¹⁷¹⁷These checks are critical, as without them a cheating prover could commit to a huge number where a limb should be and exploit the field’s wraparound. I won’t go into how it works here, but the details are on GitHub if you’re curious. There are of course other schemes that allow tighter packing with their own tradeoffs, but this is the one Claude chose.

§3.1.Accounting

Let’s now count how many limbs we’ll need to commit for a dense layer¹⁸¹⁸Doing only dense is fine, because MoE layers commit about the same number of limbs (a token’s shared and routed experts are together as wide as the dense MLP). of one request (1024 tokens):

• MLP hidden values (g_w, g_k, s and u)
• g_w, g_k, s and u are all [1024, 16384] matrices, with each entry stored in 2 limbs
• The remainders of g_w and u are two more matrices of the same shape, but with each entry stored in only 1 limb
• So (4 × 2 + 2 × 1) × 1024 × 16384 ≈ 1.7 × 10^8 limbs per layer

-  **Attention** (collapsed in[Figure 3](#fig-dense-proof) )
  - **Queries, keys, values and output** (q, k, v, o)
    - q_w, q, o and the remainders of q_w and o are [1024, 5120] matrices (2 limbs each)
    - k_w, k, v_w, v and the remainder of k_w are [1024, 1024] matrices (2 limbs each), as the model uses *Grouped Query Attention* (GQA), where its 40 query heads share just 8 key/value heads between them
    - The remainder of v_w is also a [1024, 1024] matrix (1 limb each)
    - So (5 × 2 × 5120 + (5 × 2 + 1) × 1024) × 1024 ≈ 0.6 × 10^8 limbs per layer
  - **Softmax weights** (P)
    - A [1024, 1024] matrix for each of the 40 query heads (2 limbs each)
    - Only the causal half is committed, in 64 × 64 tiles plus a little padding, so 576 keys per query on average
    - Each weight also has a remainder (2 limbs) and a flag (1 limb)
    - So (2 + 2 + 1) × 40 × 576 × 1024 ≈ 1.2 × 10^8 limbs per layer
-  **The residual stream** (x′, x′′)
  - x′ and x′′ are [1024, 5120] matrices (5 limbs each)
  - The remainders of Δ_1 and Δ_2 are also [1024, 5120] matrices (1 limb each)

• So (2 × 5 + 2 × 1) × 1024 × 5120 ≈ 0.6 × 10^8 limbs per layer

-  **Norms** (a_w, a, m_w, m)
  - a_w, a (before attention) and m_w, m (before the MLP) are [1024, 5120] matrices (2 limbs each)
  - The remainders of a_w and m_w are also [1024, 5120] matrices (2 limbs each)

• So (4 × 2 + 2 × 2) × 1024 × 5120 ≈ 0.6 × 10^8 limbs per layer
• Range checks & other bookkeeping¹⁹¹⁹ These overheads are per segment rather than per layer, so I had to average them out over the 48 layers to get these numbers.

  • The check that every limb is small commits values of its own, about 1.5 × 10^8 limbs

  • Including the previous segment’s folded row (Figure 4 ) adds about 0.4 × 10^8 limbs

  • Lookup and sum-check bookkeeping add about 0.1 × 10^8 and 0.2 × 10^8 limbs, respectively

  • So roughly (1.5 + 0.4 + 0.1 + 0.2) × 10^8 = 2.2 × 10^8 limbs per layer That’s about 7.0 × 10^8 limbs per layer. 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 find that we commit to about 3.5 × 10^(10) limbs per request. Since we pack three limbs into each field element, that’s about 1.2 × 10^(10) field elements per 1,024-token request.

§3.2.Pricing

Let’s now work out how long it takes an H100 to commit to all of this for a batch of 64 requests. FlashProve lays each request’s field elements out as tables with rows of 2^(22) elements, so each request is about 2,790 rows in all, once padded.

There are three main costs:

• Encoding. Each row gets Reed-Solomon encoded at rate ρ = 1/2, from 2^(22) elements to 2^(23). That takes one NTT per row, so 2,790 × 64 ≈ 1.8 × 10^5 NTTs per batch. An H100 can do… well, it’s not exactly obvious how many NTTs like this an H100 can do per second. The problem hasn’t been attacked as heavily as standard float FFTs or hashing. Claude Fable 5.2 estimates an H100 can do at most about 55,000 of these NTTs per second (so about 3.2 s per batch), given the absolute minimum arithmetic required for the best known algorithms today. Luckily, the final bound isn’t very sensitive to this (even if encoding were free, it would only go up by ~15%).
• Merkle trees. Each request’s encoded tables are 2^(23) columns wide. Every column gets hashed into a leaf, and then each table’s leaves are hashed up into a Merkle tree. Counting in BLAKE2b compressions (one per 128 bytes hashed), that’s aboutunderbrace(264 × 2^(23), leaves) + underbrace(76 × 2^(23), tree nodes) ≈ 2.9 × 10^9compressions per request, or 1.8 × 10^(11) per batch. ²⁰²⁰ Worked out fromFlashProve’s proof format . Password crackers have optimized BLAKE2b on GPUs for years, and hashcat (one of the fastest) does about 7.2 billion per second on an H100 PCIe.²¹²¹ Fromthis benchmark . While this isn’t a proven upper bound, I think it’s fair to say this problem has been attacked thoroughly enough that major speedups would be very surprising. Scaled up to the H100 SXM, that’s about 9.5 × 10^9 per second, which takes 19.3 s.²²²² If you aren’t aware: there are two GPUs which go by the name H100. H100 SXM, and H100 PCIe, which is a slightly nerfed version of the SXM, with only 114 SMs vs the 132 SMs on the SXM, and a lower clock (1,755 vs 1,980 MHz). In this article I’ve been taking H100 to refer to the H100 SXM, except in cases where clarification is needed.
• Proofs of work. Each batch grinds ten 28-bit proofs of work for the weight opening, and each request grinds thirty-six 20-bit proofs of work, so in total that’s 10 × 2^(28) + 64 × 36 × 2^(20) ≈ 5.1 × 10^9 BLAKE2b hashes, which (at the rate above) takes ≈ 0.5 s.

Putting this all together, we get an upper bound²³²³Assuming encoding can’t overlap with hashing, since both compete for the same integer units. In practice, encoding might be able to offload some work to the float/tensor units, but as noted above, even free encoding doesn’t shift the bound much. of:

So even if committing to the intermediate values was the only work we had to do, and we could do it with perfect kernels, FlashProve could go at most ~23x faster than it does today.²⁴²⁴Again, this is assuming hashcat’s BLAKE2b throughput is near optimal. Note that adding more GPUs doesn’t help, since we’re measuring per GPU. The total work per token stays the same, more GPUs just split it up.

To be clear, this is an estimated upper bound, but not necessarily a tight one. There are almost certainly other bottlenecks that bring it down further in practice, but this was the easiest bound I found that’s both defensible and tight enough to be useful.

§4.Conclusion #

Without protocol changes, and assuming hashcat is near optimal, FlashProve can be sped up by at most ~23x, to about 2,800 tokens per second per GPU. Since this bound isn’t tight, the achievable gains are probably a good deal smaller, but there’s plausibly still a good amount of headroom in better kernels. Even assuming this upper bound is realizable though, it’s still about 10x below what the model’s FLOPs alone would allow (“100% MFU”).

How fast is fast enough? It depends on the use case. For some methods of treaty verification, even FlashProve’s current overheads might be sufficient, as only a random sample of requests may need proofs. For others, like verifiable inference for paying customers, we’ll likely need protocol improvements before it’s commercially viable. Luckily, I don’t think the current protocol is anywhere near the best we can do. I’m excited to see how things progress over the next 6 months!