# Model Internals, part 1: Proving LLM inference on Rust, CUDA, and Lean

URL: https://www.msuiche.com/posts/model-internals-part-1-proving-llm-inference-on-rust-cuda-and-lean/
Date: 2026-11-11
Author: Matt Suiche
Tags: Provable Inference, Lean, CUDA, PTX, Rust, ICICLE, zkSNARK, Multilinear Proofs, Goldilocks, LLM


> Model Internals, part 1. Weightproof verifies complete FlashProve key, link, and request transcripts, proves dense integer-model execution with multilinear PSC and lookup forests, runs ICICLE CPU and native CUDA backends, and proves the emitted PTX fold equal to an independent SSA and Launch.runThread in Lean. With Anthropic's FlashProve, DeepMind's AlphaProof Code, SP1, SF Tensor, ICICLE, and the rest of the roadmap.

---


![Frog tells Toad that the program has a proof of correctness; Toad observes that an unread proof could have proven anything.](./images/frog-toad-proof.png)

*Cartoon by [JP Aumasson](https://twitter.com/veorq).*

Windows Internals taught a generation of systems people to stop treating the operating system as a black box: handles, objects, syscalls, memory, and the contracts between them. Model Internals is the same exercise for modern AI systems. Weightproof is part 1 because the interesting security property is not a bigger model or a faster token counter; it is knowing exactly which weights, traces, tables, instructions, and proof obligations produced a token.

This is highly experimental work, built mostly to play around and learn what verification can and cannot do. zkVM remains an interesting concept worth revisiting, and the clearest way to see its limits was to build the alternatives and measure them. The goal is not to declare a winner; it is to make the tradeoffs concrete enough to be useful.

Weightproof now checks a complete key, link, and request proof against committed model weights, rather than accepting a provider's claim about which model produced a response. The current implementation verifies exact dense integer-model execution with committed weights, residual traces, lookup tables, and output tokens; generates quadratic multilinear proofs with zero-padded witnesses and paired folding; runs those proofs on Rust, ICICLE CPU, or native NVCC CUDA; and proves the fixed kernel's emitted PTX instruction stream equal to an independent arithmetic SSA and `Launch.runThread` in Lean 4.34.1. [PR #1](https://github.com/msuiche/weightproof/pull/1) is merged as `1879dd7`, with every CI job green.

The trust boundaries matter as much as the throughput. The implementation does not yet load an 8B checkpoint, does not prove compiler lowering or SASS, and does not claim the full PTX memory model. It also does not equate the exact integer model with a floating-point serving engine. A valid proof means that the committed weights and the declared integer computation produced the checked tokens. Any difference between that computation and the served engine is a statement failure, not an optimization.

![Statement, proof, and verification flow, with differential execution, Lean, and scope guardrails.](./images/protocol-flow.svg)

## Repository map

The repository is organized around the proof statement and the evidence for it:

- `src/fp` contains the no-std verifier core, exact integer model, canonical parsers, Merkle and chain logic, multilinear PSC, lookup forests, and the optional prover backends.
- `cuda/fold.cu` and `src/fp/native_cuda.rs` contain the fixed fold kernel and its scoped FFI, including resident series and dot-product contexts.
- `formal/GpuFold.lean` contains the field, word, launch, arithmetic-SSA, and PTX correctness proofs, plus concrete non-vacuity witnesses.
- `spec/` records the exact integer semantics, proof lifecycle, security parameters, extraction review, execution environments, and PTX scope.
- `spikes/` holds FlashProve ground-truth fixtures and the WHIR evaluation artifacts used for C++↔Rust agreement.
- `tests/`, `fuzz/`, and `benches/` exercise accepted and mutated transcripts, parser robustness, and block/kernel performance. `.github/workflows/` runs the same checks plus Lean and native CUDA.

## Why a bespoke proof stack instead of a zkVM

The starting point was [Anthropic's FlashProve](https://www.anthropic.com/research/provable-inference) and its [technical report](https://www.anthropic.com/document/flashprove-technical-report): a bespoke interactive oracle proof for transformer inference, with a weight commitment, succinct proofs, zero-knowledge weights, and a Lean formalization. FlashProve's public prototype proves Llama 4 Maverick, a 400B-parameter MoE, at roughly 110 tokens/second on one H100. Its approximately 19 MB per-request proofs verify in seconds on CPU. That result demonstrates the target is practical when the proof system is built around the model's operations.

A general zkVM is a poor substitute for the matrix-multiplication core. [SP1](https://github.com/succinctlabs/sp1) proves RISC-V execution, which means paying for instruction, memory, and CPU-state semantics for every useful arithmetic operation. The evaluation recorded in `PLAN.md` rejects that path for LLM-scale matmuls and keeps a zkVM only as an optional shell for glue logic. That is not a reason to write zkVM off: it is worth revisiting for protocol glue, new precompiles, and smaller workloads where the trace overhead is acceptable. The best way to see the limitation was simply to play with real proof workloads and watch where the cost moved. The alternative was not another hand-waved circuit either: [worldfnd/whir](https://github.com/worldfnd/whir) is a candidate WHIR implementation, but it remains behind an explicit security and benchmark gate in `spec/security-parameters.md`.

The resulting split is deliberate: a Rust verifier and multilinear prover for the current dense model, [ICICLE](https://github.com/ingonyama-zk/icicle) for CPU acceleration, a native CUDA backend for larger folds, and Lean for the parts where an independent mathematical argument is worth more than another differential test.

## The statement is the security property

The verifier checks a complete execution statement, not a hash of some weights next to some output text. A block statement binds the weight commitment, the residual execution trace, lookup tables, and the output token. `spec/proof-lifecycle.md` extends that binding to `H(version ‖ commitment ‖ prompt ‖ cfg ‖ sampling ‖ tokens)`, where `cfg` covers architecture, quantization, code, and runtime parameters and `sampling` covers the decoding policy and seed. Unknown versions, non-canonical encodings, truncation, trailing bytes, a different statement, or a different parameter set fail closed with named errors.

The exact integer model defines the computation being proved: floor division, `rq`, `clamp`, `low8`, `argmax`, `isqrt`, normalization without gains, rotary projections, softmax, SiLU, sigmoid, and table generation. Range constraints make the field equations imply the intended integer arithmetic. Public rotary, softmax, SiLU, and sigmoid tables match independent Python references. Weight commitments, residual streams, and output tokens are checked by recomputation as well as by the proof transcript.

This distinction is fundamental: a proof for a different computation is not a proof of serving correctness. FlashProve has the same limitation, and the roadmap includes a measured divergence evaluation between the integer model and the serving engine. Until that exists, the statement is the truth condition, and no faster backend changes it.

For [GLP steering](https://github.com/msuiche/weightless/blob/main/docs/spec/GLP.md), the statement extension is naturally linear. A projective control vector applies $h \leftarrow h - \alpha(h\cdot\hat d)\hat d$ at selected hook points. The vector and hook metadata can be public inputs while only the base weights remain hidden. No new nonlinear gadget is required. The runtime projection differs from weight orthogonalization, $\Delta W = -\alpha\hat d(\hat d^\top W)$, which is a rank-1 LoRA; [Arditi et al.](https://arxiv.org/abs/2406.11717) describe both forms. REAP-pruned builds are rejected because deleting experts changes the circuit and invalidates the steering vector and the model identity.

## What the prover and verifier implement

The current Rust implementation executes accepted key, link, and request transcripts. It checks canonical field encodings, proof-of-work, chain-derived positions, five Merkle openings, and the algebraic claims behind BAT, FOLD, CS, and BASE. It then executes the request's lookup forest, layer claims, output head, second LIN stage, and request-own test, with exact cursor exhaustion. Accepted fixtures verify; mutations are rejected.

The arithmetic layer uses [Goldilocks](https://github.com/0xPolygonZero/plonky2/blob/main/field/src/goldilocks_field.rs) $p = 2^{64}-2^{32}+1$ and the cubic extension $E = F[X]/(X^3-2)$. A multilinear fold has the simple form

```
fold(zero, one, challenge) = zero + challenge * (one - zero)
```

Quadratic multilinear dot-product rounds emit coefficients for the evaluation of a product at a challenge, using epsilon scaling and zero-padded witness tensors. Both witness vectors fold after every challenge. The prover also emits product-relation and forest-shaped PSC proofs, with per-request statement and chain separation. Justin Thaler's [Proofs, Arguments, and Zero-Knowledge](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf) is the useful background for the sumcheck and multilinear machinery.

Two practical format changes reduce proof size without changing acceptance: dot-product batching reduces 683,360 arithmetic proofs per eight-token request to 10,930, and compact base-field endpoints reduce the two-request transcript from 67,685,664 bytes to 23,967,008 bytes, a 2.82× reduction with identical verification. `format_version = 1` binds that encoding. Independent request batches verify independently, including cross-request rejection, which is the property needed for per-client extractable verification.

## Native CUDA is a backend, not a second computation

The native backend builds `cuda/fold.cu` through NVCC and a scoped FFI. Rust handles smaller folds; native CUDA handles folds at and above 8,192 input elements. Both paths use the same field equations and produce byte-identical multilinear proofs. ICICLE remains the evaluated CPU backend; native CUDA exists because the fixed kernel is small enough to verify and fast enough to matter.

The large proof paths keep witness vectors resident on the device. Each `dot_round_kernel` folds the current pair and computes the next round's three coefficients from the folded values. The initial coefficient pass is the only additional launch, and full witnesses return only for final evaluation. Generic fold chains and dot-product proofs reuse per-thread streams and buffers across calls, with each new proof resetting logical length and current buffer before uploading fresh witnesses.

![Witnesses remain on the device across proof rounds; backend selection splits at 8,192 elements.](./images/cuda-residency.svg)

The measured results are fixture-specific, not an 8B serving claim:

| Workload | Before | Current |
|---|---:|---:|
| Small block prove / verify | 9.76 / 7.74 ms | **5.82 / 5.73 ms** |
| Larger fixture prove / verify | 18.4–23.8 / 16.7–20.5 ms | **8.68 / 8.80 ms** |
| 8,192-pair PSC proof | 2.24 / 1.74 / 2.25 ms | **2.09 / 1.66 / 2.08 ms** |
| Thirteen-challenge, 8,192-element chain | 208–241 µs | **119–130 µs** |
| Isolated create/upload/drop cycle | 183.8–246.1 µs | **21.8–22.3 µs** |

The larger fixture has four layers, feed-forward width eight, an eight-token maximum window, and a four-token input. It is explicitly not an 8B model. The small-block baseline is retained because the threshold samples were noisy; the larger threshold measurements are consistent. Rejected experiments are documented too: pinned staging regressed proving by 21.5%, direct extension-slice layouts regressed verification, and polling instead of `cudaStreamSynchronize` was neutral and removed.

## Lean closes a different gap

Differential tests show that two implementations agree. Lean shows what the fixed kernel means. `formal/GpuFold.lean` proves the fused cubic-extension fold and multilinear quadratic-round identities, canonical Goldilocks operations, exact unsigned-word addition, subtraction, 128-bit reduction, and multiplication, launch/index safety, active/inactive behavior, and non-vacuity witnesses.

The PTX model then connects the emitted instruction subset to the same arithmetic. `ptxRunThread_eq_ssa` proves the stream equal to an independent SSA, and `ptxRunThread_correct` proves active and inactive PTX threads equal `Launch.runThread`, hence the canonical fold. The proof uses separate address/load stages, C0/C1/C2 register equations, output-stage zero-input registers, and exact machine-word operations instead of one large simplification that would exceed Lean's kernel recursion limit.

![Lean proof composition from emitted PTX to the canonical fold.](./images/formal-proof-stack.svg)

The final axiom report contains only `propext`, `Classical.choice`, and `Quot.sound`. There is no `sorryAx` and no native decision axiom. The 32-bit address branch uses a kernel-checked `Nat.testBit` proof rather than `bv_decide`.

[SF Tensor's PTX work](https://sf-tensor.com/engineering/formalizing-ptx) and its [paper](https://sf-tensor.com/papers/formalizing-ptx.pdf) show why the next layer would matter: conservative PTX semantics, data-dependent control flow, memory consistency, and multi-kernel composition. Their public implementation is not available for direct reuse, and this project does not claim their memory-model coverage. Compiler lowering, SASS, and hardware behavior remain outside the current proof.

[DeepMind's AlphaProof Code](https://deepmind.google/blog/introducing-alphaproof-code/) is the other useful comparison. Its agents generated more than six million lines of Lean to verify Signal's compiled cryptographic implementation, with humans reviewing roughly one percent of the result. The important shared idea is that Lean, not the agent, decides whether a proof is valid. The targets differ: AlphaProof Code verifies a deployed protocol implementation, while weightproof verifies a proof-carrying computation and the fixed GPU kernel that accelerates it. Its [formal verification artifacts](https://google-deepmind.github.io/code-verification) are a concrete example of what broader proof coverage can look like.

## Verification evidence

The merged commit passes all of these checks locally, on `dgx1` with an NVIDIA GB10, and on GitHub Actions:

| Check | Result |
|---|---:|
| Lean 4.34.1 | Full `formal/GpuFold.lean` check, 2.28 s |
| Default Rust | 133 tests across three suites |
| ICICLE CPU | 134 tests across three suites, one CUDA-only test ignored |
| Native CUDA on GB10 | 139 tests plus every stride and resident-round check |
| no-std | `thumbv7em-none-eabi` build passed |
| PR and main CI | All jobs passed |

The native suite includes real multilinear block proving, accepted and mutated key/request fixtures, large device-resident rounds, and cross-proof context reinitialization. Rust and native-CUDA multilinear proofs are byte-identical, with SHA-256 `04d95d7500f779145f1018a711496f318d1baa257b5ebada780640a0ea92c7ea`. CI also runs Criterion benchmarks and five libFuzzer targets, including 1,583 compact-proof cases and 2,778,910 layout cases.

## What remains open

The [working todo list](https://github.com/msuiche/weightproof/blob/main/TODOS.md) is part of the security boundary. The main open items are:

- **Scale and model coverage:** an 8B weight fixture and loader, then MoE proofs with work proportional to active experts and measured expert coverage. M4 targets verifiable sampling and 128k contexts, but has no implementation claim today.
- **Proof-system evaluation:** the WHIR spike still has to clear its security and fixed-parameter benchmark gate before any commitment-building work depends on it.
- **Implementation extraction:** `spec/extraction-review.md` stages field, tensor, and Merkle extraction with hax/coq-of-Rust before full verifier extraction. The `dyn` interfaces that block extraction still need refactoring.
- **Full machine semantics:** compiler lowering, SASS, the full PTX memory model, and hardware behavior. The current PTX theorem is exact for its emitted subset, not a proof of everything NVCC or the GPU can do.
- **Serving and trust integration:** independent commitment certification, renewal chains, registry-backed model identity, adaptive-request randomness accounting, and measured divergence between the integer model and the serving engine.
- **Distribution:** a verifier CLI and release pipeline for Linux and macOS on amd64 and arm64. This is active work, not a published artifact yet.

The acceptance rules are already strict. Unknown versions and mismatched statements fail closed. Commitment renewal requires a fresh offline commitment and certificate, not a date extension. A renewed proof must bind the same model identity and revision back to an independent trust root. These rules prevent a valid-looking proof for substituted weights from becoming an acceptance path.

## References

- [Anthropic: Progress on provable inference for large language models](https://www.anthropic.com/research/provable-inference)
- [FlashProve technical report](https://www.anthropic.com/document/flashprove-technical-report)
- [FlashProve source and fixtures](https://github.com/anthropics/FlashProve)
- [SP1 zkVM](https://github.com/succinctlabs/sp1)
- [worldfnd/whir](https://github.com/worldfnd/whir)
- [ICICLE](https://github.com/ingonyama-zk/icicle) and [ICICLE overview](https://dev.ingonyama.com/1.10.1/icicle/overview)
- [Lean 4](https://lean-lang.org/)
- [SF Tensor: Formalizing PTX in Lean](https://sf-tensor.com/engineering/formalizing-ptx) and [paper](https://sf-tensor.com/papers/formalizing-ptx.pdf)
- [DeepMind: Introducing AlphaProof Code](https://deepmind.google/blog/introducing-alphaproof-code/) and [verification artifacts](https://google-deepmind.github.io/code-verification)
- [hax / coq-of-Rust extraction](https://github.com/hacspec/hax)
- [Justin Thaler: Proofs, Arguments, and Zero-Knowledge](https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf)
- [Arditi et al.: Refusal in Language Models Is Mediated by a Single Direction](https://arxiv.org/abs/2406.11717)
- [GLP format specification](https://github.com/msuiche/weightless/blob/main/docs/spec/GLP.md)
- [Rust `no_std` embedded guide](https://doc.rust-lang.org/nomicon/embedded.html)
- [cargo-fuzz](https://github.com/rust-fuzz/cargo-fuzz)
- [Criterion.rs](https://github.com/bheisler/criterion.rs)
- [NVIDIA CUDA programming guide](https://docs.nvidia.com/cuda/cuda-c-programming-guide/index.html)
- [NVIDIA PTX ISA](https://docs.nvidia.com/cuda/parallel-thread-execution/index.html)
- [NVIDIA DGX Spark](https://www.nvidia.com/en-us/products/workstations/dgx-spark/)
- [BLAKE2](https://www.blake2.net/)
- [Goldilocks field](https://github.com/0xPolygonZero/plonky2/blob/main/field/src/goldilocks_field.rs)

## Acknowledgment

Thanks to Moonshot Kimi K3.1 Pro for assisting with the research, implementation, proof decomposition, and this write-up.