levineuwirth.org/content/essays/verified-inference/index.md

---
title: "Verified Inference Between Adversaries"
date: 2026-08-29
abstract: >
  A compute operator who claims to have run a particular model can be lying, and
  the logs that would settle it are written by the party under suspicion. VerInf
  produces zero-knowledge proofs of LLM inference, bounding the information in an
  output stream that a committed model does not account for. This living document
  details what the system certifies, what it does not, and what I contributed to
  it during the MARS V fellowship.
tags:
  - ai
  - tech
  - research
  - research/machine-learning
status: "Working model"
confidence: 85
importance: 5
evidence: 4
scope: broad
novelty: moderate
practicality: moderate
history:
  - date: "2026-08-31"
  - date: "2026-08-30"
  - date: "2026-08-29"
---

A datacenter asserts that it ran a 400-billion-parameter model on your prompt. It
might have run a smaller one, an older checkpoint, or a quantized copy that
costs a fraction as much. Ordinary logging cannot settle this, because the logs
are produced by the party whose behavior is in question. Neither can a hash of
the weights: the operator can hold the right weights and still run something
else.

Similarly, assume that a treaty between two governments is reached regarding
AI research and development. Both governments claim that they are using particular
models that meet certain thresholds, have been approved by regulatory boards, etc.
The same problem applies; there is not any obvious way for one party to such an
agreement to verify the claims of the other.

This remains an unresolved gap wherever the verifier cannot trust the operator,
or the attestation stack the operator controls. Evaluations measure a model under
conditions you control, and say nothing about the model served to somebody else
afterward. Hardware-backed attestation can say a great deal about platform and
software state — but it buys that by requiring trust in a hardware root-of-trust
ecosystem, and it still does not yield an operator-independent statement about
*this* computation producing *that* output. What is missing is a way to replace
trust in the operator's execution environment with a proof an independent
verifier can check on hardware it controls.

[VerInf](https://github.com/JamesPetrie/VerInf) is a research prototype
addressing that gap, led by James Petrie at the Future of Life Institute. I
work on it as a [MARS V](https://caish.org/mars) fellow. This living document
records what the system does and does not currently prove, where the work is
heading, and which parts of it are mine.

## What the proof certifies

The naive framing — chiefly, "prove the model produced this output" — is the wrong one.
Frontier inference runs in floating point, on nondeterministic kernels, across hardware that does not
reproduce bit-for-bit. Demanding exact reproduction would make the problem intractable, and would
still answer the wrong question.

VerInf instead bounds the **unexplained information** in an output stream: the
number of bits in the output that the committed model does not account for. If
the operator swapped in a different model, the outputs it produced would be
poorly predicted by the model it committed to, and the bound rises. A cheap
substitution is therefore expensive to hide.

The intended end-to-end certificate combines three pieces, held to different
standards — and one of them is not yet integrated:

- a **transcript anchor**, binding the committed token streams to digests
  recorded independently at generation time, so the certificate is about the run
  that actually happened rather than a convenient reconstruction. *The AES and
  SHA-256 circuits for this are implemented and tested; they are not yet wired
  end to end against recorded digests.* The demonstrated runs below are therefore
  internally consistent — the scored tokens are the tokens the proven forward
  pass consumed — but not yet externally anchored to a record made at generation
  time;
- the **forward pass**, where every claim must admit exactly one satisfying
  assignment. Slack in an intermediate value would propagate through the
  remaining layers in directions nobody can analyze;
- the **surprisal bound** itself, where freedom *is* permitted, provided every
  free direction pushes the reported number up rather than down.

Upstream of the logits the prover must have no room at all;
downstream, in the short arithmetic from logits to the reported
bound, the prover may have room, so long as every rounding is forced upward.
Cheating there can only make the prover's own number worse.

A related move governs our predictor. The bound is computed against a predictor
of the deployment's outputs that the *prover* supplies.
By [Gibbs' inequality](https://en.wikipedia.org/wiki/Gibbs%27_inequality) the resulting sum
is a valid upper bound for *any* predictor, so the choice can indeed be left to the prover
entirely.

Underneath, matrix products are checked with Freivalds projections over [Ligero](https://link.springer.com/content/pdf/10.1007/s10623-023-01222-8.pdf)
commitments, which are hash-based — so there is no trusted setup, and the construction is plausibly post-quantum^[Future research intends to make this statement of "plausible" post-quantum security into one of "definitive" post-quantum security.].

## Where trust is required

The **prover** wants confidentiality: weights, activations, and both token
streams must not leak. The **verifier** wants soundness: the reported bound must
be genuine. Their interface is a public claim list stating what kind of
computation was performed — which reveals the model architecture, though not the
weights.

Under the protocol's soundness assumptions and a correct verifier
implementation, the prover need not be trusted for correctness: prover
deviations can cause false acceptance only within the protocol's soundness
error, and otherwise cause verification to fail. Those are real assumptions,
not decoration — soundness rests on the cryptographic primitives, the challenge
generation, the verifier's own parser boundaries, and the per-challenge bound of
the chosen configuration, which is a deployment parameter rather than a fixed
property. The verifier's trusted base is deliberately small and shares no code
with the prover, which narrows that surface without eliminating it. VerInf has
not had a full security audit.

The arrangement this enables between mutually distrustful parties: each runs its
own verifier on its own hardware, and neither has to trust the datacenter where
the proving happened.

## Results on record

First, the single-chip results, which predate my involvement.

| | Llama-4-Maverick | Llama-2-7B |
|:---|:---|:---|
| Parameters | 400B MoE, 48 layers, 128 experts committed per layer | 7B, 32 layers |
| Transcript | 1000 tokens, **all hidden** | 1000 tokens |
| Prove | 14.3 h, 78.1 GB GPU peak | ~44 min, 11.2 GB peak |
| Verify | 17.7 h, 20 CPU cores, 40 columns opened | ~23 min, 10 columns |
| Proof size | 93.6 GB | 1.44 GB |
| Bound | 0.880 bits/token | — |

All on a single NVIDIA DGX Spark. The committed witness for the Maverick run is
roughly 7.2 TB, streamed at the working set rather than held.

At 0.880 bits per token against a 202,048-token vocabulary, the proof accounts for about 95% of the information a
token could carry. That is not "the model produced this"; it is "very little
here is unexplained by the model that was committed."

## What I have contributed thus far

Parallelizing the prover across GPUs is named future work in the paper, and it
is the direction I am working in. It runs into an immediate problem: you cannot
measure a cluster you do not yet have access to, and partitioning decisions have
to be made before the hardware arrives.

My first deliverable was the measurement scaffolding that parallelism needs.
I built a **dry-run profiler** that predicts a
proving run's time, memory, bandwidth, and proof size *before* running it, from
a workload manifest plus measured hardware constants, and exposes the dependency
structure a future scheduler will consume:

- a **manifest contract** — one record per tape operation, with two independent
  producers (an exact tape-walker that runs where the prover runs, and
  closed-form builders in pure Python that cross-check it);
- a **cost model** in per-claim accounting form, carrying the production
  expressions from the paper's cost appendix;
- a **claim-level dependency DAG** with critical path and width profile, which
  is what tells you how much parallelism actually exists;
- a **partition scorecard** that maps claims onto *N* shards under competing
  strategies — contiguous tape ranges, pipelined layers, expert-sharded — and
  scores them.

A profiler is only as good as its predictions, so validation came in two
rounds. The first was retrodictive: predict the archived Maverick run from a
synthetic manifest plus the development box's measured constants, then compare
against what that run actually recorded.

| quantity | predicted | measured |
|:---|:---|:---|
| witness rows | 108.7 M | 109.27 M |
| proof size | 93.1 GB | 93.6 GB |
| opened-column GPU payload | 34.8 GB | ~35 GB |
| verifier peak RSS | 76.1 GB | 75.7 GB |
| proof dump time | 751 s | 756 s |
| prove wall-clock | 3.0 h floor / 9.9 h aggregate | 14.26 h |

Prove time is deliberately a *bracket*, not a point estimate. The floor is the
bandwidth-bound target the design should reach after planned reorganization;
the aggregate is calibrated on today's code. The gap between bracket and
measurement largely reflects itemized implementation overhead, and so functions
as a work-list rather than an unexplained residual.

The second round I ran end to end myself, on hardware the tooling had never
seen: a single rented B200, the class of machine the multi-GPU effort actually
targets. One morning and about eleven dollars of GPU time later:

- the calibration suite filled a complete machine profile from scratch, every
  constant measured on the box with its provenance recorded (headline: 29×
  the development box's memory bandwidth);
- the exact tape-walker ran against real tapes for the first time and
  **cross-checked clean against the closed-form builders — zero flags**: every
  claim count, witness slot, linear constraint, and quadratic product matched
  within the documented expected set, and the per-row witness layout agreed
  with the prover's own accounting row for row;
- the extracted Maverick manifest reported **109,273,513 witness rows,
  against the production run's measured 109.27 M** — the profiler reproducing
  reality, not merely its own model of it;
- the cost bracket priced on measured Blackwell constants puts the
  routed-projected Maverick proof at S=1000 at a **254-second floor** on one
  B200, the dominant terms riding memory bandwidth and tracking that 29×
  ratio — which is what the cost model's scaling story says should happen.

I also corrected the cost model's RMSNorm row to the wrap-free bracket
constants, bringing it into line with the paper's own analysis.

### Splitting the enrolled weights without touching the verifier

The first piece of real multi-GPU work is now on a review branch, and the result
worth reporting is not a speedup. It is that there is no new trust surface.

Under enrollment the weights are touched by exactly two per-proof passes, and
both are exact field sums over ranges of rows. A sum does not care which device
computed its addends. So the enrolled-weight work can be cut across devices and
recombined into a proof that is **byte-identical** to the one a single device
would have produced — not equivalent, not accepted under some new rule, but the
same bytes. The unmodified Rust verifier accepts it because, as far as the
verifier can tell, nothing happened.

That matters more than the phrasing suggests. Parallelism normally costs
protocol surface: a new aggregation step, a new commitment, a fresh argument
about why the combined object is as sound as the original. Here it costs none,
by construction, and [the trust boundary](#where-trust-is-required) stays
exactly where it was. The acceptance gate passed 4/4 on hardware — including a
Rust ACCEPT on a sharded proof — at every N=2 cut and with deliberately
non-nesting N=3 stage cuts.

Byte-identity also makes correctness cheap to test. If the sharded output must
equal the single-device output bit for bit, the roles can be run sequentially on
one GPU and the proof bytes diffed; no cluster is required. The whole gate ran
on a rented A40 for about forty cents, against the eleven dollars the B200
calibration session cost. That partly retires the problem this section opened
with. After this branch, only *speed* needs hardware I do not have. Correctness
does not.

### A retraction

The same B200 session produced a finding I later had to withdraw: an apparent
interconnect bottleneck that turned out to be almost entirely an artifact of my
own traffic model. Nothing was wrong with the machine; something was wrong with
what I had assumed about it.

I record it because it is the discipline the whole exercise exists to enforce.
A profiler that only ever confirms its author is not a measurement instrument.
Predictions go out before the measurement, and get corrected in public when the
measurement disagrees — otherwise the numbers above would be worth very little.

The correction is now upstream rather than only narrated here. The original
scorecard reported roughly 950 GB per sweep of cross-shard traffic and returned
a binding verdict on interconnect; with the traffic model corrected — settlement
vectors reduce to per-shard scalars rather than shipping whole — the same
configuration moves 2.4 to 2.8 GB per sweep, and communication is negligible at
every bandwidth swept. Nearly all of the original figure was my own modeling
error. The retraction is part of the merged record, not a footnote to it.

### What is upstream, and what is not

**Merged code** — the dry-run profiler and its parts: manifest contract,
extractor, cost model, execution DAG, partition scorecard; the RMSNorm
cost-model correction; and, as of 30 August 2026, the calibration suite, the
machine-profile tooling, and the corrected traffic model.

**Publicly inspectable evidence** — the B200 session archive, the extracted
manifests, the calibration logs, and the measured machine profile are all in the
repository. An earlier version of this section asked you to treat the figures
above as reported by me rather than independently checkable. That caveat has
been discharged: the inputs that produced them can now be read, and the
cross-checks rerun.

**On a review branch** — the stage-aware weight-split model, the
verifier-transparent weight split itself, and per-variable packed-source
provenance for the storage mode: three commits on
[`weight-split-model`](https://github.com/JamesPetrie/VerInf/tree/weight-split-model),
pushed and readable, but not merged. They are pending review at the next project
meeting, and should be read as committed work in the open rather than as
accepted work.

**On agent assistance.** Implementation was agent-assisted. I owned the research
direction, the cost-model derivation and checking, the experimental design, the
validation, and the review; generated code was kept only after it was tested and
cross-checked. This is project-wide practice rather than a personal one, across contributors,
as part of how the fellowship's compute is used. Much of the repository's
history records it in commit trailers; the convention is changing, and my newest
commits carry none. That is precisely why it belongs here in prose rather than
left to be inferred from metadata that may or may not be present.

::: {.work-entry-links}
[Merged pull requests](https://github.com/JamesPetrie/VerInf/pulls?q=is%3Apr+author%3Alevineuwirth) ·
[Upstream repository](https://github.com/JamesPetrie/VerInf)
:::

## Where this goes next

The immediate step is a port to 2–8 GPUs, and the reason is not that more GPUs
sound better. Multi-device proving is what lifts the ceiling on model scale,
context length, and mixture-of-experts breadth — the dimensions along which a
single box runs out first.

The honest projection carries the same bracket as everything else here. The
anchor is a **254-second floor for the routed-projected Maverick proof at
S=1000 on one B200**: a floor, not today's code, and it assumes the
reorganization the cost model already itemizes. The sharding numbers have already moved once, downward, and the correction is
worth more than the original figure was. An earlier version of this section
reported 3.95× of a possible 4× at four devices. That model quietly allowed an
imbalance in one stage to cancel against the other. It cannot: the fold and open
stages are separated by a transcript barrier, so each stage's slowest shard sets
its own pace. Modeling the stages separately gives **1.90× at two devices and
3.47× at four**, saturating near 3.75× as the coordinator's own fresh-path work
becomes the wall. These are modeled zero-overhead ratios under a stated
stage-split assumption — the tool prints a 2.00×–1.79× sensitivity band on the
two-device case — and none of them is a ceiling or a promise.

That saturation is what orders the work rather than merely describing it: split
the weights first, then the fresh rows, then attention for long context. The
wall moves each time. And even at saturation this is the 254-second floor
divided by less than four, which is minutes rather than seconds.

The first wall in practice was not the GPU at all. Streaming the 226.5 GB
enrolled block from the rental's shared network volume capped proving at roughly
1,523 seconds however many devices were attached — 0.17× of the floor, with the
disk setting the pace. Local NVMe recovers about 1.9× at two devices; only
keeping the block resident in HBM reaches the modeled ratio, and residency is
named engineering work rather than a free consequence of adding GPUs.

No multi-GPU speedup has been measured. Every ratio above is a prediction priced
on measured constants, from a model validated against one archived run and one
live machine — good enough to plan against, and the first measurement is the
next milestone.

Beyond that, fleets of 64–128 GPUs are what an order-of-magnitude larger model
would require. That figure comes from the same cost model and has not been
validated at that scale.

## Current Limitations
While VerInf looks promising, there are currently limitations:

- **No security audit.** It is a research prototype.
- **Proof Size** — 93.6 GB at full scale. This is a real deployment
  obstacle, not a rounding error.
- **0.880 bits per token is not zero.** For some applications that residue is
  fine; for others it is not, and the paper is explicit that tightening it is
  open work.
- **Soundness is a per-challenge bound** (about 2⁻¹⁶·⁶ in the demonstrated
  configuration), raised by opening more columns at a measured cost in
  verification time. It is a deployment choice, not a fixed property.
- **The claim list reveals the architecture.** The public claim list states what
  kind of computation was performed, so layer counts and expert breadth are
  visible to the verifier even though the weights are not.
- **No multi-GPU speedup has been measured.** The weight split is verified
  byte-identical on hardware, but every scaling ratio here is modeled. The first
  end-to-end multi-device timing is the next milestone.
- **The transcript anchor is not yet demonstrated end to end.** The AES and
  SHA-256 circuits are implemented and tested; binding them against
  independently recorded digests is not yet shown.

## Why this matters for assurance

The reason to care is not that datacenters are presumed dishonest. It is that
"trust us, we ran the model we said" is the current state of the art, and it
does not scale to a world where the stakes of that claim keep rising —
third-party evaluation, regulatory audit, compute governance, any arrangement
where an inference claim carries weight and the parties are not aligned.

Verified inference is one approach to a general question: how do you establish
trustworthy claims about an AI system when the system, the operator, and the
evaluator may each be untrusted? Cryptography attacks it from below. Evaluations
attack it from above. Neither is sufficient alone.