proofinfer

A Llama inference engine in Rust with zero external dependencies, built around a claim that is usually made and rarely justified: that it computes the right thing.

The work

The engine is the small half. The rest is the evidence:

Differential testing against the PyTorch reference from llama2.c — six configurations, every logit at every position.
Byte-identical output against run.c, a third independent implementation in C.
Mutation testing on both halves of the suite, so neither the harness nor the tests can be quietly incapable of failing.
A machine-checked Verus proof of KV-cache index safety.

Results

Differential, 6 configurations6/6 · 1.0e-5

Real stories15M weights200/200

Greedy output vs run.cidentical

Mutation: harness · test suite10/10 · 21/21

Verus, --no-cheating24 verified

Rust tests, debug and release75

Throughput, single-threaded835 tok/s

Documentation

Testing — how correctness is established, and how every check was shown to fail.
Performance — throughput, the 8-lane dot product, and the gap left by -Ofast.
Design — architecture, the trusted computing base, and what is not verified.