The verifier is 122 lines long, and five of them are pub use.
That is not minimalism for its own sake. The verifier is a façade over a record — a Trace — and the record has to carry enough to rebuild the computation from nothing. Hand it to somebody else, on their own machine, with the network unplugged, and ask them to recompute the answer from the record alone.
If they land on exactly the same bits, you never needed to trust the first computation. You needed to trust the arithmetic.
That is the whole idea underneath the work I have been doing with Hologram, and it is much older than software. Verification is a round trip. Run it, record it, run it backwards, compare.
A log records that something happened
Everything the industry has built for evidence over the last decade records the same fact: that an event occurred.
A reviewer opened the ticket. A pipeline passed the gate. An agent produced an output and a human said it looked fine. The event is logged, timestamped, and archived. Whether the judgment was correct is nowhere in the record — and because the review effort is invisible and unrewarded, nobody can price the risk either.
“Human in the loop” has quietly become “human clicks approve.”
More dashboards and better checklists will not fix this, because they are all answering the question “did the event happen?” when the question is “is the outcome right?”
Math cannot answer the second question by being a cleverer reviewer. It answers it by changing what a reviewer is signing. Not “I read this and it looked fine,” but a statement precise enough that a machine can check the artifact against it, bound to the artifact’s content hash, and replayable by anyone who wants to try.
Running it backwards
Let be the execution that folds a compile unit into a grounded value and a certificate, and let be the replay that unfolds a trace back into a certificate. The property I want is that doing both is the identity:
The equality is bit-for-bit on the certificate. Not “the same answer, within tolerance.” The same bits.
flowchart TB
I[Compile unit and input] --> F[run - the fold]
F --> G[Grounded value and certificate]
F --> T[Trace]
T --> U[certify_from_trace - the unfold]
U --> C[Recertified certificate]
G -. bit-identical .-> C
In our Prism standard library this is prism::replay::certify_from_trace. The verifier takes a Trace and re-derives a Certified value from it. Three details make it work, and all three are the opposite of what you would guess:
- It does not re-run your deciders. It re-derives the certificate from the contents of the trace.
- It does not compute a hash. The content fingerprint is data carried by the trace, computed at mint time by the hasher the author chose and passed through unchanged. The verifier never folds bytes.
- It validates the trace’s structure on the way past: step indices monotonic and contiguous from zero, no zero targets, no empty trace.
That last point is what keeps the verifier small. prism_verify is a façade — the crate adds zero behavior and only a namespace. A verification consumer depends on that crate alone and never on the runtime, so the attack surface of “verify this for me” is a hundred lines instead of the whole system.
And the round trip is not a hope. It is an assertion:
let trace: prism::replay::Trace = grounded.derivation().replay();
let recertified = certify_from_trace(&trace).expect("trace is well-formed");
assert_eq!(
recertified.certificate().content_fingerprint(),
grounded.content_fingerprint(),
"QS-05: re-certified fingerprint must equal the source fingerprint",
);That property has an identifier because it is a conformance requirement rather than an implementation detail. QS-05 is replay equivalence: the round trip is bit-identical. QS-03 says verification is local — it runs on your own hardware, with no network access. TC-06 says verification reaches no application-author service, so the thing that produced the artifact has no ability to help, hide, or interfere.
That last one matters more than it sounds. A verification step that can call back to the producer is not a verification step. It is a second opinion from the same mouth.
Nothing checked against itself
The failure mode I keep running into is a verifier that only agrees with the thing it is checking. It is worse in AI systems for a specific reason: the code is now generated faster than anybody can read it, so the temptation to let the machine grade its own homework is enormous. A test that checks a kernel against the project’s own reference evaluator proves internal consistency. A hash checked against a constant the project produced itself proves the project is self-consistent. Both are green. Neither tells you anything about the world outside.
The rule we use in Hologram is short enough to repeat: external ground truth, not self-reference. Every part is validated against an authority we did not author.
| Part | External authority |
|---|---|
| Hash axis (BLAKE3) | the upstream BLAKE3 reference crate |
| Content addresses (κ-labels) | uor-addr, itself externally validated, plus TC-05 replay |
| Numeric kernels (matmul, conv, norm, softmax) | the ONNX operator spec and ONNX backend node test data; IEEE-754 |
| Model ingest (GGUF, ONNX) | the format specs, plus cross-tool agreement with independent loaders |
| Quantization | the GGML and ONNX quantization reference |
| Whole-graph execution | an independent runtime’s outputs — ONNX Runtime, PyTorch |
The same discipline appears in Prism itself, where every public item in the codebase backlinks to the wiki section that defines it, and the wiki links are mechanically validated in CI. A broken anchor fails the build. The documentation is not a promise about the code; it is checked against it.
I wrote about a version of this before, in The Green Test Passed for the Wrong Reason — a security test that was green because the image happened to be harmless, not because the runtime enforced anything. Every claim needs a mechanism, a scope, and a witness that breaks when the mechanism breaks. Otherwise the claim is decoration.
What was the artifact supposed to do?
Replay alone is not enough. A trace proves what happened. It says nothing about whether what happened was right.
For that you need a second ingredient: a machine-checked statement of what the artifact is supposed to do. Not a docstring, not a comment, not a checklist — a statement in a proof assistant that a small, trusted checker can verify mechanically.
Then the reviewer signs the statement, not the code. And the work divides like this:
flowchart TB
S[Artifact] --> L[Machine-checked statement]
L --> M[Machine verifies the code against the statement]
L --> H[Human confirms the statement says what was meant]
H --> A[Attestation bound to the artifact hash]
A --> E[Stake settled against the outcome]
- Type safety, permission boundaries, exact arithmetic, data formats, “the build matches the spec” — mechanically provable. No human reads code.
- Business logic and intent — the machine checks the code against the statement; the human confirms the statement is the right statement.
- Quality of free-form output, design choices, whether an answer is good — human judgment, attested and staked.
One property makes the middle row affordable: verified pieces compose, and everything is addressed by its content hash. A component proven once never needs rechecking wherever it is reused. Verify once, reuse everywhere. That is a real compute saving, not just a compliance story — the reuse is safe because the identity of the thing you verified is the identity of the thing you are reusing.
Where proofs run out
This is the part I want to get exactly right, because it is the part that gets oversold.
A proof guarantees that the artifact matches what was written down. If the statement is wrong, it faithfully proves the wrong thing.
There is no way around this. A proof checker cannot tell you what you ought to have wanted. It tells you that the thing you asked for is the thing you got.
So the human does not disappear. The human moves. Instead of reading thousands of lines to discover what the code does, the human reads a few precise statements and asks the one question no machine can ask: does this say what I meant?
That is a better question than the old one, and it is worth more human attention per minute than the old one. The old question — is this code correct? — required reading everything and remembering all of it. The new question requires understanding one thing well and being accountable to it.
I want to keep two phrases apart, because they have different timelines and different buyers. Reproducible is not the same as correct. A system can be perfectly replayable and still be doing the wrong thing, and a system can be correct and irreproducible. The mathematics buys the first. It does not buy the second.
Inference doesn’t replay
Everything above assumes the computation being checked is deterministic. For most software that is a choice you can make. For a neural network it is not: floating-point inference on different hardware produces slightly different results, so nobody can independently recompute your record and confirm it. You are left trusting the machine that ran it, which is where you started.
R4 is our attempt to remove that excuse. The serving contract — we call it D11 — is that served kernels use integer and table lookups only: add, subtract, shift, compare, table reads. No floating point and no multiplier instruction. If that holds, the same artifact on any machine produces the same output, and the entire round-trip argument extends to model inference. Not “the model probably said something similar.” The same bytes.
Where it stands, honestly: pre-alpha. Zero of eight milestones complete, four in progress. The D11 serving engine is bit-exact against the float path, with equal NLL on 3,072 targets, and the artifact is 11.9 MB — that is a real result and it is the part that matters for this argument.
The language quality is not there. The best chat stack is a 19.9M model measured in bits-per-byte, not a model that holds a conversation. The 214M base improved from 2.90 to 2.073 NLL on a development split, and rewrite and summarize work while code and math do not. No tested geometric mechanism has yet beaten a matched ordinary control — a stack scored 1.998 against a matched transformer’s 2.011, which is parity, and parity is not a win.
The cost side gets the same honesty. A measured product-table emulator used 4.3 times the energy of its float comparator, so no general energy advantage is established. The negatives are kept as evidence rather than deleted, and the project asks whether this combination can reach a useful model and records the answer either way.
That last property is the point. If the answer turns out to be no, an honest no is still a result, and it is worth more than an unfalsifiable yes. I have written about this discipline before in What Result Would Make Us Stop?.
Money is what makes somebody look
Even with perfect statements and exact replay, you still need a human for the third category — quality, intent, whether an answer is good. And you need that human to actually do it.
This is where most “human in the loop” systems quietly fail. Review effort is invisible, unrewarded, and unprovable, so a rubber stamp is indistinguishable from a careful review, and neither one is measurable. Nobody can tell whether oversight happened, which means nobody can price the risk, which means nobody has a reason to care.
The mechanism I believe in is mostly legal rather than technical. The reviewer signs an attestation bound to the artifact’s content hash, stakes value behind it, and the stake settles against the outcome: if the artifact later fails under replay, the stake is cut. Seeded defects — canaries — reward real attention and expose rubber-stamping, because a reviewer who never catches the planted defect simply does not get paid.
The mathematics gives you the thing that was checked and the thing that was meant. The money makes sure somebody looked.
The part I have to do by hand
A verification system that checks itself proves nothing.
You can verify a computation by running it backwards, but only if the record you kept is complete enough to reconstruct it, and only if the check is made against something you did not write yourself.
The rest is arithmetic, and arithmetic is the easy part. The hard part is deciding what the statement should say — and being willing to be held to it.
Every piece of this still ends with a person writing down what the artifact is supposed to do, and somebody else agreeing to be accountable to that sentence. I have not found a way to make that step cheaper, and I have stopped expecting to.