Five steps. Each one exists because skipping it is a way that real systems have already gone wrong.
Nothing on this page requires knowing how any of it is implemented. Each stage links to results that exist and can be run.
Decide in advance exactly what the system is allowed to do, and write that decision down before it acts.
Why it is a step. If permission is worked out at the moment of action, or inferred afterwards from what happened, there is nothing independent to check the action against.
Does not establish. The bound, not conservation. No liveness, availability, or Byzantine model; crash is global in the Lean model, and per-replica crash is only exercised in the bounded checks. The pr…
Does not establish. It is terminal-observation safety, the value the driver reads is within the cap, not an all-intermediate-state invariant, and it carries no liveness or wait-freedom. The kernel che…
Does not establish. One defect in one server built for this study, not a measurement of deployed systems and not a claim about how often authorization layers and executors diverge. Mediation held thro…
The system acts, and the action it takes is the one that was authorised, not merely one that resembles it.
Why it is a step. The gap between the action a policy approved and the action that actually ran is where several of the failures below live.
Does not establish. This is a demonstration against an authored mock, not a measurement of real servers. It does not test HTTP transport, prompt injection, or token scope, and a passing result does no…
Measure what actually changed, by looking at the files, records or state afterwards.
Why it is a step. A record of what a system intended reads exactly like a record of what it did, until something measures the difference.
Does not establish. A property of one synthetic, deterministic testbed under injected faults, not a measurement of any deployed safeguards product and not a rate that transfers outside this harness. T…
Check the observation against the permission, mechanically, using something that was not part of doing the work.
Why it is a step. Checkers can be wrong, and two checkers that share a source are wrong together.
Does not establish. That either judge is reliable, or that the direction generalises beyond this corpus. The sample is small; the per-answer correctness labels are assistant-adjudicated, not human; an…
Does not establish. Not a claim that agreement between judges carries no information, and not a general law about language-model judges. It is a property of these judge checkpoints on these 600 items …
Does not establish. One defect in one framework, in the metadata a finished run records about itself. It says nothing about the correctness of any model score, nothing about how often the condition ar…
Does not establish. That the library is defective for its purpose. A lax parser tuned for triage is a different artifact from one built to be exactly round-tripping; this is that a round-trip theorem …
Someone else can re-run the check later, from the record alone, and get the same answer.
Why it is a step. Evidence that only its author can reproduce is testimony. Evidence anyone can re-derive is a different kind of thing.
Does not establish. That the opaque hash function is SHA-256, that the recorded decision was correct, or that the formal definitions match the prose specification. It is tamper-evidence at the model l…
Does not establish. Bit-for-bit reproducibility on other hardware, which is untested and reported UNKNOWN rather than upgraded. It does not establish code correctness, buggy-but-faithful code still ve…