Archived page from the earlier OMEGA site (October 2026). Its figures and statuses have not been re-checked since and may be out of date. Current research: Research. Current evidence record: Evidence.
Every important public claim, with the same twelve fields: how far the evidence reaches, where it stops, and whether the check has ever been seen to fail.
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.
Each record opens to its twelve fields. The grade and the one-line finding are visible closed.
git clone https://github.com/repowazdogz-droid/omega-n1-permit-membership && cd omega-n1-permit-membership && python3 reproduce.pynpm install && ./run.shmake clean && make check./verify.sh --quickpip install inspect_ai && inspect eval repro.py --model mockllm/modeleval $(opam env --switch=capctl-iris) && make verifypython scripts/agreement/build_report.py && python scripts/agreement/sweep_writeup.pypython scripts/build_report.py && python scripts/recompute.py && pytest -qpython scripts/build_report.py && python scripts/recompute.py && pytest -q./demo.sh && make experimentsgit clone https://github.com/repowazdogz-droid/omega-lean-proof && cd omega-lean-proof && lake build && lake env lean probes/AxiomProbe.lean./run_all.shpython3 -m pytest tests -q && python3 -m commons.report _canonical/gpt-5-mini _canonical/gpt-4.1-mini _canonical/gemini-2.5-flashpython3 scripts/verify_records.pymake setup && make allpip install -e . && python3 -m pytest tests/ -qmake lean axioms z3 controls # and make rl for the learning adversary, about 90 scd formal && make ecc.checkPYBAMM_DISABLE_TELEMETRY=true python minimal_reproducer.py --output reviewer-outputNo record matches that filter.
Questions posed and not answered, listed at full weight because a residual that is hard to read is a residual that gets forgotten. These are the eight from the worked case; the collective-bound exhibit carries its own.
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.
OPEN19 repositories, each with what it establishes, what it does not, what has to be trusted, and the command that reproduces it.
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.
Two evaluation logs compared deterministically, distinguishing 'unchanged' from 'cannot tell'.
Mediation held; binding did not.
A harness detects a tool hidden from discovery yet reachable through the call surface, on a mock built to show it.
A verifier re-derives a training run bit-for-bit; cross-hardware re-derivation stays UNKNOWN, not claimed.
A sealed, replayable decision record whose tamper-evidence is machine-checked.
A monitor reports intentions as outcomes.
A deterministic, severity-ranked semantic diff for four high-risk engineering formats, no LLM calls.
Four kernel-checked theorems about a JSON parser and serialiser, with a differential over 120,000 inputs.
A pre-registered study of whether LLM agents produce the collective failure that per-agent rules permit.
Governance properties routed to the checker whose logic fits, with the LLM judge's score sealed beside the proof.
A small power-control IP verified with open tools; two injected defects invisible to every specification-derived property.
A grader for recorded verification outputs that reports what a run explored, not the verdict it printed.
The formal core behind the collective-bound result: Lean 4 (six theorems, no axioms), Z3 (eleven sealed verdicts), a learning adversary, negative controls.
Released means the fix is in a tagged release. Merged means it is on the default branch but not verified in a tagged release. Open pull request means an Omega-authored change awaits upstream action. Open issue means a report remains open without a merged fix. Maintainer acceptance is review of one change, not endorsement of Omega.