Verifiable AI Inference on DEOS

Version 1.0, June 2026

Summary

This paper describes a working system that produces LLM inference outputs accompanied by a cryptographic certificate identifying everything that went into the run. The certificate is produced by the operating system rather than the application, so it cannot be forged or stripped by the model operator. Anyone with the public weights and tokenizer can re-execute the run and confirm byte-for-byte that the certificate is honest.

The shipped implementation runs karpathy's stories15M, a 15-million-parameter Llama2-style transformer, inside a DEOS userspace process. It also runs a Q4_K_M quantized Mistral 7B from the same code path on the same substrate. The system is slow compared to GPU stacks. That is the trade we are making. In exchange, the model output has a provable origin.

Why this matters

There is a class of decisions where "the model said so" is not a sufficient audit trail. Loan approvals. Medical triage. Trade execution. Anywhere a regulator can later ask "what exactly did the system do, and how do you know," the operator needs an answer that does not depend on their own log files.

The standard answer today is application-layer logging plus a signed transcript. This works until the day someone subpoenas the production environment and finds out that the operator could have edited the transcript before signing it. The signature proves the operator signed something. It does not prove they signed what actually ran.

The gap is that conventional operating systems treat the contents of an inference, the weights, the prompt, the tokenizer state, the per-token outputs, as application data. The kernel does not see it. If you want a provable record of an inference, you have to ask the application to make one, and now you are back where you started.

DEOS treats this as a kernel problem instead.

How DEOS handles it

DEOS is a deterministic event-sourced operating system. The kernel logs every syscall, interrupt, and context switch into a per-CPU ring with Lamport ordering. A recorded run can be replayed on the same hardware and produce the same bytes. Under tighter compilation and floating-point rules, the same byte equality holds across CPU vendors.

Sitting on this substrate is an Execution Certificate, or ExCert. An ExCert is a kernel-emitted record that ties together four things:

1. A declaration of inputs the application says fully determined its output.
2. BLAKE3 hashes of those inputs, computed by the kernel, not the application.
3. The bytes the application produced as output.
4. A content-addressed pointer to the syscall and event log for the entire run.

The application calls one syscall to declare what its output depends on. The kernel hashes the declared inputs, captures the output, and writes everything into content-addressed storage. The certificate is open, not zero-knowledge. What it gives you is provenance, not privacy.

What the certificate binds

For an LLM inference, the binding is:

Inputs:

Outputs:

Each field is hashed separately so a verifier can ask narrow questions. Was this output produced from the prompt the user actually sent? Was it produced by the same weights I have? Each question gets a yes-or-no answer that does not require trusting the others.

The architecture hash deserves a note. It is the BLAKE3 of a canonical string listing the model's structural parameters: number of layers, attention heads, hidden dim, vocabulary size, sequence length, positional encoding family. This pins the structural assumptions independent of the weights. Two runs with the same weights but different layer counts would produce different architecture hashes, so the certificate will not falsely claim equivalence.

Making it actually deterministic

Greedy decoding handles the algorithm side. At each step, pick the highest-logit token. No sampling, no temperature, no top-k or top-p. Same prompt, same weights, same code: same tokens, every time.

The algorithm side is the easy half. The hard half is floating point. A naive f32 matrix multiply on the same inputs can produce different bytes on different CPUs because reduction order is not standardized, FMA contraction varies by compiler flag, and denormal handling differs across vendors.

DEOS handles this through the rules documented in the Floating-Point Determinism Specification:

• IEEE 754 round-to-nearest-even is the only mode exposed
• SIMD reductions use a fixed, declared order
• FMA contraction is decided at compile time and the choice is bound into arch_hash
• Denormals are flushed to zero with a consistent policy
• The compiler is pinned by a toolchain manifest that is hashed into the build

Under these rules, the same run produces identical bytes on the same machine across reboots. Under the additional cross-host conditions in the Replay Proof, the byte equality holds across CPU vendors.

What is actually shipped

The userspace binaries doing this work today:

deos-infer-attest: the first proof of concept. Three test prompts, six ExCerts emitted, all verified valid by the off-DEOS tool. Small sentiment classifier, not a real LLM. Exists to demonstrate the certificate mechanism end-to-end.

deos-llm-attest: the real version. Runs stories15M inside a DEOS userspace process. Generates coherent children's stories at the TinyStories level. Emits one ExCert per generation with the binding above. Pure no_std Rust, libm for transcendentals, no SIMD, greedy decoding.

deos-mistral-attest: same code path scaled up. Runs Mistral 7B with Q4_K_M quantization. Full forward pass, same ExCert binding. Throughput is limited by CPU f32 matmul.

tools/excert-verifier: the off-DEOS verification tool. Reads a kernel commitment file, re-hashes the recorded inputs, and confirms the certificate is well-formed without needing DEOS running. This is the path a regulator or counterparty would use.

The kernel side adds two features beyond the basic ExCert. Glass-box execution attestation records the side-effect chain of the run, so a verifier sees not just inputs and outputs but the intermediate steps. The glass-box tampering test shows that modifying a single weight at one layer changes the certificate hash in a way that lets a verifier localize which layer was modified, not just detect that something was.

There is also a tiered execution model. The same model can run on three paths: CPU baseline, CPU with SSE4.1, and GPU. Each tier emits its own ExCert with the tier identity bound into arch_hash. So a verifier can tell a CPU run apart from a GPU run, and the operator cannot present a fast GPU result and claim it was the same run as a slow CPU one.

How a verifier actually checks a certificate

Three steps. Two of them require nothing from DEOS.

Step 1: re-hash. Given the same weights blob, the same tokenizer, and the canonical architecture string, the verifier computes BLAKE3 over each and compares to the values bound in the certificate. Takes seconds.

Step 2: re-run. Using the bound prompt and the same model artifacts, run the inference code on any machine following the floating-point discipline. The output tokens should match byte for byte. Takes whatever the inference takes (tens of seconds for stories15M on CPU, longer for Mistral 7B).

Step 3: replay the syscall trace. Optional, but the strongest of the three. For Challenge-tier certificates, the kernel stores the full syscall trace in content-addressed storage. The verifier can replay the recorded events against the same binary and observe the same kernel-visible behavior. This requires either a DEOS instance or a reimplementation of the DEOS event semantics.

Steps 1 and 2 cover most real-world verification needs. A regulator who wants to know "was this loan approval really produced by your stated model on the prompt you logged" can answer that question entirely from public artifacts and a CPU.

Honest scope

This is a real system but a small one.

stories15M is a real transformer. Real attention, real autoregressive decoding, real RoPE. It is also 15 million parameters, which is tiny by 2026 standards. Mistral 7B is the first scale-up. Larger models are gated on GPU support, which is gated on resolving the Polaris VFIO issues documented separately.

Only greedy decoding is supported in the deterministic path. Stochastic sampling would require declaring an RNG seed and binding it into the certificate. That is a straightforward extension. It has not shipped.

Pure-Rust f32 matmul without SIMD is slow. Single-thread stories15M generates one to five tokens per second. The SSE4.1 tier is faster. GPU is the goal. None of this affects the certificate property, but it does limit which workloads can use the system at all today.

Cross-host byte equality has been demonstrated for the kernel build itself across Apple M3 Max and Linux x86, and at runtime across AMD and Intel CPUs. For inference specifically, the byte equality follows from the same rules but has been measured at smaller scale so far.

The verifier trusts BLAKE3, the Rust compiler, and the math libraries. All of these are public and reproducible. A verifier who does not trust a given component cannot use the certificate.

Why this is a different thing from a faster inference stack

Throughput-optimized inference and verifiability-optimized inference pull the architecture in opposite directions.

Fast inference uses fused kernels, mixed precision, stochastic sampling, and tensor parallel reductions whose order is whatever the scheduler picks. All of these break determinism, either directly or by leaving the reduction order unconstrained. There are good reasons to do all of them in a setting where the output does not need to be verified after the fact.

Verifiable inference uses fixed reduction order, fixed precision, declared compile flags, and deterministic sampling. The runtime is slower. The output is provable.

The set of workloads where the second matters more than the first is not all workloads. It is the workloads where a third party may later need to confirm what actually ran. That set is small today and growing.

What is next

Near term: Mistral 7B at full production binding with the certificate; stochastic sampling with seed-bound certificates; GPU tier for stories15M once the Polaris work resolves.

Medium term: larger Llama-architecture models on the same certificate path; cross-vendor GPU determinism (NVIDIA and AMD parity); a verifier UI that does not require running a tool from the command line.

Longer term: multi-step agent runs where each step emits its own certificate and the chain is signed end-to-end; integration with DEOS Tessera so an inference certificate can be settled directly on an Ethereum L2.

Closing

The system described here is slow. That is a real cost. In exchange, an inference run on DEOS carries a record that lets any third party answer the question "how do we know that is what actually happened" by re-hashing the inputs, re-running the code, and optionally replaying the syscall log. The answer does not depend on trusting the operator.

There are workloads where that is worth more than a 10x or 100x speedup, and workloads where it is not. For the first set, this is a primitive that can be built on today.

References

• DEOS Determinism Model. /whitepapers/determinism-model
• DEOS Floating-Point Determinism Specification. /whitepapers/fp-determinism
• Cryptographic Verification of Deterministic Replay in Multi-Core Operating Systems. /whitepapers/replay-proof
• DEOS Phase Kernel-4: Scientific Proof of Deterministic Replay. /whitepapers/scientific-proof
• DEOS Model Standard (DMS-1) Specification. /whitepapers/dms-1
• DAV: DEOS Agent Verification. /whitepapers/dav
• DCO: DEOS Computing Oracle. /whitepapers/dco
• DEOS Tessera: Verifiable Shared Sequencer for Ethereum L2s. /whitepapers/tessera