Every result carries a grade recording how far the evidence reaches, a statement of what it does not establish, and where possible a command that re-derives it from a public clone.
How to read a grade. PROVEN follows from stated premises inside a named frame. MEASURED is empirical with a stated sample. OBSERVED was witnessed in one instance with no claim about how often. OPEN is a question posed and not answered. A grade is a statement about the evidence, not about importance.
The note was never checked against the list of permissions that had actually been granted. It only had to look right. Anything that could read a public list of what fixes exist could write itself a valid-looking note, and the program would act on it.
Does not establish. It is not a break-in from outside. It needed nothing secret, but it also needed the ability to run code on that machine already.
One asymmetry, stated. 13 of the 13 findings below re-derive from a public clone. This one does not: its artifact is not published, so the bundle carries records and pointers rather than a runnable check. That is the weaker kind of evidence and it is labelled as such.
Decide in advance exactly what the system is allowed to do, and write that decision down before it acts.
A write of 100,000 bytes executed under a policy that capped writes at 4,096 bytes, while 66 of 66 tests passed, an independent replay verifier returned VERIFIED, and a checked complete-mediation invariant held.
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 throughout; what failed was the binding between the authorized operation and the executed one. Policy adequacy is separately not established, and two counterexamples covering it are retained unfixed.
npm install && ./run.sh
Total spend never exceeds the cap in any reachable state of the escrow protocol, proved in Lean for any finite set of replicas and any non-negative amounts.
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 proof holds relative to the transition system being a faithful abstraction of the protocol, which is argued, not machine-checked.
make clean && make check
A capability meter never exceeds its cap over every concurrent interleaving of charge operations, proved in Iris concurrent separation logic for any cap and any finite list of operations.
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 check was not re-run in this pass; axiom-freedom rests on the committed assumptions audit plus a live search finding no admitted goals.
eval $(opam env --switch=capctl-iris) && make verify
The system acts, and the action it takes is the one that was authorised, not merely one that resembles it.
A start permit assembled entirely from public registry facts, with its reference number derived by the authorizer's own function and committed to no ledger, was accepted by the bounded executor and the registry-named transform was applied; the target's bytes changed.
Does not establish. One defect in one program built for this study. Not a measurement of deployed systems, and no claim about how often authorisation records are treated as evidence of authorisation. Not a break-in: producing the forgery requires the ability to run code as the same user, and such an actor can edit the target directly without any record. The minimal fix establishes that a membership check closes this specific defect; it does not establish at-most-once execution, atomic consumption, or independent measurement of the effect.
git clone https://github.com/repowazdogz-droid/omega-n1-permit-membership && cd omega-n1-permit-membership && python3 reproduce.py
Measure what actually changed, by looking at the files, records or state afterwards.
Over 10,000 injected events, a monitoring arm recorded 1,026 actions as prevented and all 1,026 executed; an in-series arm consuming the same events, evaluator and policy recorded 6 of 9,880.
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. The agent environment is deliberately trivial so that what is measured is the pipeline rather than model behaviour.
./demo.sh && make experiments
Check the observation against the permission, mechanically, using something that was not part of doing the work.
A widely used C JSON library does not preserve numbers across a serialise-and-reparse round trip: its number pipeline is lossy by design, printing with limited precision and comparing re-reads by tolerance rather than equality.
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 is false of the target, not a quality judgement.
./verify.sh --quick
In a widely used evaluation framework, the same failing run reported a different number of completed samples depending only on the order its scorers were declared in: 6 of 6 under one ordering and 4 of 6 under the other, with both runs ending in a success status.
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 arises in practice, and nothing about other evaluation frameworks. The upstream design decision to score errored samples is separate and was not disputed.
pip install inspect_ai && inspect eval repro.py --model mockllm/model
Across 600 items and 171 judge pairs, judge errors correlated positively in 171 of 171 pairs at mean phi 0.567, and the correlation between pairwise agreement and accuracy fell from 0.824 to 0.077 once the algebraically forced component of agreement was removed.
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 against a machine-checkable answer key. Ground truth here is a key, not human labelling, and the mechanism behind the second experiment is reported as open rather than settled.
python scripts/agreement/build_report.py && python scripts/agreement/sweep_writeup.py
At 45 answers, a judge with zero disagreements has an agreement interval spanning its whole range; the perfect score reads as 'no counterexample found at this sample size', not as demonstrated reliability.
Does not establish. That the ensemble judge is reliable. A degenerate interval at the endpoints cannot express uncertainty, and at larger scale even ensemble judges are imperfect.
python scripts/build_report.py && python scripts/recompute.py && pytest -q
Two language-model judges scoring the same 45 GSM8K answers disagreed with the ground truth in opposite directions: one systematically too strict, the other too lenient.
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; and two of the three judges also generated answers in the set, so self-preference is uncorrected.
python scripts/build_report.py && python scripts/recompute.py && pytest -q
Someone else can re-run the check later, from the record alone, and get the same answer.
Tampering with a sealed, hash-linked decision record forces a hash collision: the canonical encoding is injective, the chain is append-only, and detection follows in Lean without a collision-resistance axiom.
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 level, not a claim about any deployed system.
git clone https://github.com/repowazdogz-droid/omega-lean-proof && cd omega-lean-proof && lake build && lake env lean probes/AxiomProbe.lean
A training run's final loss and trajectory re-derive bit-for-bit from its recorded inputs on one machine; cross-hardware re-derivation is left as UNKNOWN, and not claimed.
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 verifies, nor result quality nor accountability.
./run_all.sh
Questions posed and not answered. They are listed at full weight because a residual that is hard to read is a residual that gets forgotten.
An actor who can run code as this user edits the target directly and needs no permit at all; equally, they can append a well-formed start permit to the ledger. The successor does not create an unforgeable token.
Explicitly out of scope. Not weakened or strengthened by the repair.
OPENNo process has been killed between the consumption commit and the write. The ordering argument is sound and untested.
It is the cheapest remaining test and it has not been run. A scheduled consumer runs unattended, which is exactly the regime where a killed process matters.
OPENEvery writer must use the ledger transaction. That is convention, not enforcement.
A writer that ignores the lock defeats the at-most-once guarantee. The auditor detects the resulting sequence disagreement after the fact; it does not prevent it.
OPENA moved clock moves the time-to-live window.
Carried as an assumption in the trusted base, named there rather than tested.
OPENAtomic replace and durable flush are assumed, not tested.
A crash must leave the original intact. That property rests on the platform and is carried as an assumption.
OPENThe successor has never executed anything outside a sandbox.
Manufacturing a live eligible condition means deliberately corrupting a real scheduled job. Not done, not worked around.
OPENThe sequence double-count in the frozen ledger transaction is measured, understood and deliberately not fixed.
Editing it would break the freeze that makes the predecessor citable evidence. The successor refuses on detecting it instead.
OPENNothing establishes that the property generalises to a transform that is not idempotent and not byte-derivable from a backup.
The bound is real and it is narrow. The narrowness is the finding, not a caveat on it.
OPEN14 artifacts, each stating what it establishes, what it does not, and the command that reproduces it. 3 of them are the bundles behind the worked case.
A concurrent capability bound holds over every interleaving, machine-checked with no axioms.
A compositional safety invariant holds for all finite N, machine-checked.
The transfer session is deadlock-free and crash-safe by typing; the budget bound is not expressible in it.
A budget bound (spend within cap) holds for all reachable states, machine-checked.
Two off-the-shelf LLM judges fail in opposite directions; a zero-disagreement judge's agreement interval is degenerate.
A read-only auditor flags silent validity failures in evaluation logs.
The full research record, including fourteen projects and the failure taxonomy this work is organised around, is at how checks fail and projects.