Towards Proving Frontier-Scale LLM Inference

How to read the numbers: every figure here is one of four kinds. It is measured on our own runs, derived by arithmetic from measured figures, projected from our cost model, or reported by others. In the text we say which. In tables, projected values are set in italics. The results repository lists every number with the run it comes from.

The short version

A proof of inference lets a provider show that an output came from a declared model on a declared input, without handing over the weights. In AI verification, a verifier can ask for such proofs on a random sample of logged requests. A provider that ran anything other than the declared model cannot produce them.

Cost has been the standard objection. Estimates in the verification literature range from about 10,000x the cost of the inference [Petrie 2026] to 500,000x [Baker et al. 2025]. We built an open prover to find out where that cost goes.
Our prototype proves greedy decoding of a quantised Llama-3.1 8B: prompt and answer, every layer, from the embedding table to the chosen token. On one H100, a request with a 4,096-token prompt and a 512-token answer takes 1.0 to 1.5 hours to prove, or $3.37–5.01 at list price. Checking all the proofs takes two minutes on CPU cores, without a GPU.
How that compares to serving depends on the shape of the request. Serving the same request on its own takes 3.4 seconds on vLLM and 9.1 seconds on HF Transformers, so proving it currently costs about 1,100x and 400x as much. Most of that gap comes from the prompt: a server processes prompt positions far faster than it generates tokens, while the prover pays the same for both. Proving 512 answer tokens without prompt reduces the ZKP overhead to 46x to 122x. For verification we think the more useful number is the price of a proof, because the verifier only proves a sample: at one proof per 10,000 requests, checking a million requests a day costs about $340–500 a day.

Most of the current proving time does not go into cryptography. The proof system accounts for about 5% of the total time. The rest goes into building the table the proof commits to, much of which still runs on the CPU. We believe engineering could bring the proving time for this request down closer to twelve minutes, and witness extraction would need the same treatment. That work suits AI unusually well, because every change can be checked byte for byte against a CPU reference.

Our prototype has clear limits and is not production-ready. The proofs are not yet zero-knowledge in the formal sense: the weights are hidden behind a commitment, but the proof system adds no blinding. And a provider would have to serve exactly our quantised arithmetic, which leaves the three benchmarks we ran within their standard error. The last section lists what separates the prototype from proving what providers actually serve.

What it costs today

What we prove, in plain words: given the prompt and the answer, every token of both went through every layer of the committed model, from the embedding table to the output layer, and every generated token is the one the model ranked first. The precise statement, how the prover works and how far to trust it follow later in this note.

We proved two requests end to end on one H100: a 4,096-token prompt and a 16,384-token prompt, each followed by 512 generated tokens. We prove each request in pieces we call segments: one transformer layer over a block of up to 512 positions. Each segment gets its own proof, and the verifier checks that the pieces fit together.

Like any STARK prover, ours writes every intermediate value of the computation into a large table and commits to it by hashing it into a Merkle tree. The cryptographic part, which we call the proof system, is that hashing plus the checks and spot-check answers the verifier needs. Everything else is preparing the table. The proving time comes as two numbers. The first is the wall-clock time of our pipeline, which works on two segments at once so that preparing one overlaps with proving the other. The second adds up every step without that overlap, and we report it as an upper bound. Neither includes recording the model’s intermediate values in the first place, which we list on its own line as witness extraction.

Compared to serving

A prover pays about the same for a prompt position as for a generated one. A provider, however, processes the prompt in one parallel pass, about two orders of magnitude faster per position than it generates tokens. So the ratio depends on the shape of the request, and it grows with the prompt.

All ratios compare one proved request with the same request served on its own. The ratios use the proving loop.

Compared to the unquantised model

A provider would have to serve exactly the arithmetic the proof constrains, int8 matrix multiplications with bf16 everywhere else (described in detail below), so its quality matters as much as its speed. Our harness runs the same bf16 intermediates and the same roundings, in the same order as the prover constrains them, against an fp32 control on the same items, with a paired standard error per task:

While perplexity rises by 7%, none of the three task scores moves beyond its standard error. A plain dynamic int8 quantisation, of the kind a provider might already serve, costs 5.0% perplexity on the same items. The same configuration costs 14.6% on the much smaller Gemma 3 270M, so these results will not transfer to every model.

Where the time goes

Proving a segment takes four steps. The prover lays out the recorded values as columns of the table. It adds extra columns that tie some of those values to precomputed tables, which is how we prove bf16 operations and range checks cheaply; we call these lookup columns. It hashes the table (the commitment). Finally, it checks the constraints between the columns and produces the answers to the verifier’s spot checks.

On the GPU, the proof system takes about 5% of the summed proving time. On a serial pass over one token block, generating the lookup columns takes 42% of the time, the base trace 35%, reading the recorded values and setting up the segment 12%, and the proof system 4.6%. Without GPU offloading, the same pass takes 6.4 times longer and the proof system is 84% of it.

We also measured the CPU/GPU differences per phase on a one layer segment of the 8B model.

End to end on the single layer, the GPU backend is 5.3x faster than the CPU reference, and 46x faster on the cryptographic steps after hashing. Most of the remaining time goes into preparing the table, which still largely runs on the CPU. Put as speeds, the whole pipeline proves 1.25 positions per second, the proof system alone could keep up with 16, and hashing alone with 27. Closing that gap is ordinary engineering (GPU kernels, memory layout, pipelining), with no change to the cryptography.

Our cost model

We chose a commit-the-trace prover partly because its cost is easy to reason about. The prover’s work is committing cells (one entry of the prover’s table), which is mostly hashing, and how fast a GPU hashes can be measured. That gives a model with two factors:
throughput (positions per second) = R / c
where R is committed cells per second, a property of the hardware and of how much of the prover is included, and c is committed cells per proved position, a property of the circuit that can be counted from the model’s shape.

Cells per second

We measure R at three levels on an H100 with Blake2s:

• The commitment alone (interpolation, extension, Merkle hashing) runs at 2.1 billion cells per second. This is the ceiling for this proof system on this card.
• The proof system (commitment plus constraint evaluation, quotients and FRI) runs at 1.3 billion cells per second. This number only moves if the proof system changes.
• The full proving loop, which adds trace generation, the lookup columns, reading the witness and building each segment, runs at 99 million cells per second. This is our current engineering, and it is the number most likely to move.

At 79 million cells per position, these give the 27, 16 and 1.25 positions per second above (on a 4,096-token run).

Cells per position

Our layout splits a request into segments of one layer over a block of S = 512 positions, attending to the C earlier positions of the prefix. A segment consists of components. Each component commits a fixed number of columns over a number of rows that follows from the model, rounded up to a power of two, so the cells of a segment are the sum over its components of rows times columns. Appendix B gives the formula for every component. For Llama-3.1 8B at C = 4,096, the shares are:

These add up to 2.72 million cells per position and layer, or 87.1 million over the 32 layers for the last block of the 4,096-token request.
Two things follow from our cost model. Attention is the largest component whose cost depends on C, so it is the main one that grows with context (other than that, it is only the boundary tree). And the number of weights appears nowhere. A Freivalds check commits the activations it reads, and the weights sit in a preprocessed tree that every proof reads. What grows with model size is the width and depth of the activations, which is why a 405B model costs about 16 times as much to prove as the 8B, and not 50 times.

How well it predicts

We checked the count at three sizes: the 8B and a 13B end to end, and one layer segment of the 70B’s shape with synthetic weights at a 128-position block. Each was reproduced to the cell. Two further block lengths of the 8B came within 0.6% of the predicted cells.

What frontier scale would cost

Everything in this section except the 8B row is projected. We assume a larger model is proven exactly as we prove the 8B, segment by segment on one H100 at today’s measured throughput; other designs and further engineering would move these numbers down. Times are proving time for the same request (4,096-token prompt, 512 generated tokens), excluding witness extraction. The last column assumes that proving scales linearly across cards. Our layout allows this once the witness exists, because segments are independent proofs, but we have not measured it.

The 405B model has fifty times the parameters of the 8B and costs about sixteen times as much to prove, for the reason given above. At the rate the proof system already sustains, the 405B request would take about 1.3 hours, roughly where the 8B is today with our current engineering.

Mixtures of experts

Each token in a mixture of experts uses only a few experts, but a block of 512 positions touches most of them: 73 of 128 on the one router we measured (Qwen3-30B-A3B, which routes the same way as the 235B). The proof has to cover every expert a block touches. Because weight checks are cheap, this costs less than one might expect:

The Qwen3-235B row uses the measured routing; the others assume tokens are spread evenly over the experts. In committed cells, Kimi K2 comes to about 2.1x a dense model with the same active parameters. The committed table of expert weights grows with the total parameter count, and our throughput was measured on a model whose weight table is small next to the rest, so these rows are lower bounds. Note that DeepSeek-V3 and Kimi K2 use multi-head latent attention, which we count under an assumed layout; the layout these models are served with would cost 5–19% more cells per position. We have implemented neither the router nor latent attention.

Context and memory

Cost per position grows with context because attention does: for the 8B, 79 million cells per position at a 4k context and 105 million at 16k, and the 405B grows by the same third. The amount of memory used by the prover scales with the committed cells. The 16k run peaked at 97% of the H100’s memory, and a single layer segment still fits at a 24,576-token context at 98%, which is roughly the 8B’s context limit on one H100 today. At 32k tokens, the attention output’s accumulator, which gains a bit each time the context doubles, no longer fits in the field. Width costs memory too: one layer segment of the 70B’s shape only fits at 128 positions, and then uses 66% of the card. We have not tried a 405B segment, and we have not projected any model at a 128k context.

Three changes would relieve memory. Shorter blocks use less of the card but cost more per position, most of all in proof size, which is 6.3 times larger per position at 256 positions than at 1,024. Committing keys and values once per key/value group instead of once per attention head would save 3.5% of a position’s cells at 4k and 9.4% at 16k for the 8B, and up to 13% for wider shapes. Streaming the prover, and in particular the attention tiles, is what would help most.

Assumptions behind the projections

• Architecture: Llama- and Qwen-shaped blocks with RMSNorm, SwiGLU, RoPE, dense full-prefix attention and a power-of-two head dimension. Gemma’s embedding normaliser, QK-norm and local/global attention, sliding windows and logit softcaps are not covered.
• Keys and values: our prover commits a copy per attention head, not per key/value group (see above).
• Dimensions: the formulas are exact for power-of-two dimensions that divide evenly into our layout, as Llama-3.1 8B’s do. Other shapes are padded; Qwen2.5-14B’s 40 attention heads, for example, are padded to 64 in two components.
• Configuration: we project the configuration we ran (512-position blocks, our softmax, our five reductions), not the cheapest possible one. Several of these are design choices that may not be the right ones at scale.
• Memory is not modelled.

Related Work

Published figures for proving LLM inference span five orders of magnitude, from a few thousandths of a token per second to a reported 195 tokens per second. Engineering explains only part of that spread. The systems prove different statements on different models, count different things and run on different hardware.

What is proved. The weakest statement is one forward pass over a fixed input. It proves the logits at every position, but not which token was chosen (zkLLM, zkPyTorch and OpenLLM below; zkGPT and Jolt Atlas prove the same kind of statement). The next is a complete decode over a key/value cache, with the emitted token proved to be the argmax, so that the proof is about the output text (DeepProve, Attestable and our prover). VerInf proves something different: an upper bound on the information in the observed tokens that the committed model does not explain.

In which arithmetic. We use int8 matrix multiplications with dynamic per-token scales and bf16 lookups; DeepProve uses 12-bit integers; VerInf uses int64 fixed point at scale 212. The quality cost of that arithmetic belongs next to every throughput figure.

Who has to be online, and what is hidden. Most schemes are non-interactive, so anyone can check a proof later without the prover. VerInf is interactive: the verifier takes part while the proof is made, which works between two parties but not for a public record. Hiding differs too.

What is counted. Some papers report total proving time, others tokens per second. A prompt position and a generated position cost a prover about the same but cost a server very different amounts, so prompt length matters. So does whether witness generation is inside the reported time. DeepProve’s tokens per minute count all positions of one concatenated pass and exclude witness generation [DeepProve, §3.1 and Table 2]. Our proving times exclude witness extraction too, which is why we report it on its own line.

Attestable also reports 53–77 tokens per second for Gemma-4-31B on one H100 [Attestable]. Two families of proof systems appear in the table. Sumcheck-based systems (zkLLM, OpenLLM, DeepProve) commit only the inputs and outputs of each layer and reduce the intermediate values round by round. Their cost is mostly field arithmetic, and all but zkLLM were measured on CPUs. Commit-the-trace systems (VerInf and ours) write the whole computation into a table, commit it with a hash and spot-check it. Their cost is mostly committing the table, which suits GPUs, although in our prototype today most of the time still goes into generating the table. Attestable has not published which family it belongs to.

How the prover works

This section gives the precise statement, how a request is split into proofs, the arithmetic and the proof system, and how far the prototype can be trusted.

The statement

For our prototype, the statement in plain words at the start of this note is:
Given the published prompt ids and the published continuation, the continuation is exactly what greedy decoding of the committed quantised Llama-3.1 8B produces from that prompt: every layer of every position, from the embedding row to the argmax, with the residual stream bound across layers and the key/value cache bound across token blocks.
The public input is the token ids and a 32-byte commitment to the weights. The tokens could be kept private as well: the statement would then say that some tokens, whose encryption matches what the certifier recorded, were produced by the model.

How the proof is split

We prove a request in segments. A segment is one transformer layer over a block of up to 512 positions, attending to all earlier positions. A 4,096-token prompt with a 512-token answer is 9 blocks of 32 layers, plus two output-head segments that prove the argmax for the answer block and for the last prompt position: 290 segments, each its own STARK. The verifier checks every proof and then checks that they chain. Every residual stream and key/value cache that one segment hands on must have the Merkle root that the next segment committed to; the first layer’s embedding rows must match the published prompt; the emitted tokens must match the published answer; and every proof must refer to the same model commitment. Appendix A walks through a full run and lists the sixteen bindings between components inside a segment.

The arithmetic

ZKPs are based on finite fields, and those handle integers well and floating point badly, so no existing system proves floating-point inference as it is served. Each fixes an integer or fixed-point arithmetic, and the proof is about that arithmetic. Ours is:

• Matrix multiplications in int8: activations per token with a dynamic scale, weights per output channel. This keeps matrix multiplication native to the field.
• Dequantisation of each accumulator to bf16 through a chain of three correctly rounded steps (round half to even), so that general bf16 scales can be proved. The output head uses power-of-two scales, which collapse the chain to one rounding.
• Everything else in bf16: the norms (with a balanced-tree reduction) and the activation function, with the exponential and the reciprocal as lookup tables keyed by the bf16 value.
• Attention scores as an integer softmax: queries rounded to 12 bits and keys to 11 under a power-of-two scale per head, with a 9-bit numerator.
• The attention output rounded straight to a 12-bit integer, which saves one rounding before the output projection.

Its quality cost is measured in “Compared to the unquantised model” above.

The proof system

The prover is a commit-the-trace STARK built on StarkWare’s open-source Stwo library, a Circle STARK over the Mersenne-31 field [Stwo; Haböck et al. 2024]. Every intermediate value of the computation is written into the columns of a large table, the trace. The columns are committed with Blake2s Merkle trees, and the verifier checks the constraints between them at random points. Lookups, which carry the bf16 operations and the range checks, use LogUp [Haböck 2022]. Five sumcheck-style reductions take the largest components out of the committed table and hand the verifier a claim about them instead: the attention key tiles, the dequantisation, the residual stream, the Freivalds checks and the attention output. Together they remove 38% of the committed cells without changing the statement.
Matrix multiplications with the weights are checked with Freivalds’ algorithm [Freivalds 1977]. Instead of recomputing C = AB, the verifier checks A(Br) = Cr for a random vector r, which costs matrix-vector products instead of a matrix product. The int8 weights sit in a preprocessed Merkle tree, committed once.

Security parameters

We use Stwo with a blowup factor 2, 100 FRI queries, no proof-of-work grinding, and Blake2s. Stwo’s own accounting puts this at 100 bits of security, under the standard conjecture on FRI soundness.

Zero-knowledge

The proof system we build on adds no random blinding to the committed trace. A proof opens the committed columns at its 100 query points and at one out-of-domain point, and without blinding those openings reveal information about the values underneath, activations and weights alike. Per proof, that is a negligible sample of the model. Still, when we say the weights stay hidden, we mean hidden behind a commitment, not hidden by a zero-knowledge proof. We left blinding out because it does not change the cost we set out to measure. The overhead of a blinding prover is an open measurement.

How far to trust it

We have two kinds of evidence. First, the CPU backend is the reference and the CUDA backend has to produce byte-identical proofs; every shape we recorded has the same digest on both. Second, a suite of 236 negative controls over five targets, each of which tampers with one value (a witness cell, a weight, a root) and requires the verifier to reject it for the reason the control was written for. All of them were rejected as designed.
To be clear, this is not an audit, and our roadmap includes a legible restructuring into smaller, auditable components. Until that changes, we treat the prototype as an instrument for measuring cost, and nobody should deploy it as a verifier.

What this means for verification

Here is how proofs would slot into a near-term protocol for inference verification. A network certifier in the provider’s datacenter records the encrypted traffic into and out of each inference node. Later, the verifier picks random requests from that record and challenges the provider to show that they came from the declared model. Today the challenge is answered by recomputing the request on physically isolated hardware. A proof answers the same challenge, and nothing else in the protocol has to change.

Random sampling

The certifier logs each request as it is served. After logging, each request is selected for a proof with probability p. A provider that answers m requests with an undeclared model, in any pattern and over any period, escapes with probability (1 − p)m. At p = 1% it can cheat about 460 times before it is caught with 99% confidence; at p = 0.01%, about 46,000 times. Read the other way, 44 proofs drawn from a batch of any size catch a provider that faked 10% of it with 99% confidence. This is the arithmetic behind the random challenges in provable data possession [Ateniese et al. 2007].
The verifier pays only for the sampled fraction. At the measured cost of one 4,096-token request ($3.37 to $5.01 on an H100 at list price), proving 0.01% of a million such requests a day costs about $340–500 a day.
Two conditions have to hold: the draw must be unpredictable to the provider, and the provider must commit to its answers before the draw. Sub-sampling pushes the same idea inside a request and proves only some layers or some decode steps of a sampled request. It needs the same two conditions, and one more assumption: that cheating is spread across the request. A single faked layer is only a 1-in-32 draw.

Who has to be trusted

TEEs and activation checks are cheap, and for many settings they are the right tool; TEEs are a sensible starting point for a first agreement. What they cost is trust: in a hardware vendor, in a third party, or in a tolerance. A proof moves that trust into cryptographic assumptions and into code that both sides can read. That is also why the code needs an audit and, ideally, formal verification: bugs in deployed proof systems have let provers prove false statements before.

Roadmap & next steps

Our prototype proves an idealised setting: greedy decoding, a public architecture, and one quantisation chosen for speed. Below is what stands between it and proving an inference in a frontier datacenter, followed by what it would take to scale. No open-source system we know of closes all of these gaps.

What deployment needs

The prover runs on the GPUs the provider already has, the verifier runs on a laptop, and flaws can be fixed by an update. Before a proof can answer a verification challenge, though, four things have to be in place:

• The parties agree on the statement: which model, which arithmetic, and how tokens are chosen.
• The proof is tied to the certifier’s record, so that it refers to traffic that was actually served.
• The implementation is audited by someone the other side trusts, ideally with its critical parts formally verified.
• The provider serves the arithmetic the proof constrains.

From our statement to what providers serve

• Sampling. We prove greedy decoding of exactly 512 tokens. Providers sample with a temperature and a top-p cutoff and stop at an end-of-sequence token. Either the sampling step is proved from a seed the provider commits to before decoding, or the statement follows VerInf and bounds what the model does not explain.
• Arithmetic. Providers serve bf16 or fp8, not our mix of int8 and bf16. Either providers adopt a provable arithmetic, or proofs cover bf16 matrix multiplications and softmax, which is expensive enough that we would pair it with sub-sampling.
• Non-determinism. Greedy decoding is not reproducible on the stacks we measured: three runs of one prompt on HF Transformers, with the same weights, in the same process and with sampling off, gave two different continuations. A provider can pin its execution (Hawkeye shows that NVIDIA tensor-core matrix multiplications can be reproduced bit for bit on a CPU once their rounding, subnormal handling and accumulation order are characterised [Hawkeye]), or the statement can absorb the non-determinism, as VerInf’s does.
• Batching. We prove one request at a time. Servers batch, and vLLM serves 16 concurrent 4,096-token requests 8.5 times faster than one at a time. Almost all of our cost is per position, so how much a prover gains from batching requests together is an open question.
• Text, not token ids. Our public input is token ids. A provider receives text, adds a system prompt and sometimes tool definitions, applies a chat template and a tokeniser, and detokenises its output. Both ends sit outside our proofs today, as do tool results a provider inserts mid-conversation. The turns of a multi-turn session would currently be unrelated proofs.
• Binding to recorded traffic. Nothing yet ties a proof to what the certifier recorded. This is where proofs meet network taps: the tap records a hash of the inputs and outputs, and the proof has to be about those same inputs and outputs.
• Other architectures. Sliding-window and local/global attention, logit softcaps, expert routers and latent attention each need extra work. We would rather build a library of optimised primitives that architectures compile to than one prover per model.
• Hiding the architecture. The verifier rebuilds the table layout from public parameters, so layer count, widths and head counts are public. A provider that will not publish its architecture needs a statement in which the shape is a private input, possibly through recursion.

Scaling

• Several cards. Once the witness exists, segments are independent proofs, so a request can already be spread over several cards. We have only measured one.
• Sub-sampling segments. A provider could commit to every segment’s boundary roots first and then prove a random subset. What is missing is the protocol around it: the commitment before the draw, and the draw itself.
• Context and memory. A streaming prover or smaller statements (see above).
• Proof size. 18.5 GiB for the 4,096-token request and 109 GiB for the 16,384-token one, checked in two and fourteen minutes. Under random sampling a verifier checks a few hundred proofs a day, so we have not built proof aggregation, and we do not think it is on the critical path for this setting.
• Auditable code. The prototype was written for measurement, not legibility. We plan to split it into small components that can each be audited.

Engineering with AI, and why soundness is the hard part

A proof system like ours is deterministic: the same constraints over the same witness give the same proof. That makes prover optimisation unusually safe to hand to AI. Given a trusted CPU reference, an AI can profile the prover and rewrite it freely, as long as every proof still matches the reference byte for byte; randomised test inputs stop it from overfitting to a fixed set of proofs. We built our GPU backend this way, and we expect the same method to close most of the gap between 1.25 and 16 positions per second, and to help spread proving across cards.
Changing the cryptography is harder. A new reduction, a cheaper binding between layers or a sampling argument can each save far more than engineering can; Freivalds’ check alone makes checking a matrix multiplication around 200 times cheaper in one recent implementation [Doukhan]. But a constraint system that accepts every honest run can still accept a dishonest one, and testing on honest runs will never show it. Catching that takes negative controls, audits and, ideally, machine-checked proofs of soundness. Starting from a statement formalised in Lean and a target soundness bound, we think AI could propose such improvements and prove them sound at the same time, with the engineering to follow.
This is also where our prototype is weakest: our soundness evidence is human review and negative controls. We think three things should be built as a public good, independent of any one prover: a specification of what an inference proof must bind, a corpus of negative controls that any prover can be run against, and eventually machine-checked constraint systems.

Work with us

We think proofs of inference should be developed in the open. Verification between parties that distrust each other only works if every side can inspect the verifier, and that makes it work for a nonprofit. SASH is building a home for it as part of its wider work on international AI verification.
The work ahead has three strands. The first is engineering the prover down, with AI doing much of the work, and finding out how far sub-sampling can substitute for it. The second is measuring at frontier scale, where we have only projections so far. The third is closing the gap between what provers prove and what providers serve: floating point, tokenisation, real serving stacks and the binding to recorded traffic. We consider the third the most important.

We are hiring and want to work with researchers, AI companies and mission-aligned organisations on the prover, on measurement or on deployment.

Appendix and References

Appendix A-C and the references, see here.