§ 5

What Omega found

Each case is one system and one claim its owners relied on. Omega built an independent way to check that claim, ran it with controls that had to be able to fail, and reports what the evidence established and where it stops. Standing is stated on every case: public where a report or package is public, internal where it is not.

SUPPORTED: The independent evidence agrees with the claim, inside the frame stated.
CONTRADICTED: The independent evidence disagrees with the claim; a witness is preserved.
INCONCLUSIVE: The evidence cannot decide the claim as stated, and the reason is recorded.

Scientific and numerical software · PyBaMM · Public

Does this battery model conserve the lithium it says it conserves?

A battery model ran to completion on every revision and lost 2.4% of its lithium

The system said: Solved, on every revision. The then-under-review pull request #5524 changed nothing.
The evidence showed: 2.44% of the lithium drifted on every revision, at every refinement. The missing term was named, and a project contributor confirmed it.

Why it matters. Nothing in the test suite measured conservation, so nothing in the suite could ever have caught this. Anyone using the model for a quantitative result had a systematic error that no green run would reveal.

CONTRADICTED×3 The case, with what it does not establish

Software whose output gets acted on · pandapower · Public

When this power-flow solver reports that it converged, did it?

A power-flow solver reported convergence for transformer types it does not support

The system said: converged=True.
The evidence showed: 994,686 per unit on a 0.4 kV bus. Four unsupported transformer types skip the gate that rejects the other ten.

Why it matters. A convergence flag was being read as this answer is usable. For four transformer configurations it meant nothing of the sort, and nothing in the output said so. Ten other unsupported types were rejected correctly, which is what makes the gap easy to miss.

CONTRADICTED INCONCLUSIVE The case, with what it does not establish

AI agents and the controls around them · Agent permission boundaries · Public artifacts and one private record

Did the system do what it was permitted to do?

What a mediation boundary establishes, and what it does not

The system said: Limited to 4 KB. 66 tests passed. Replay: VERIFIED. 1,026 actions prevented.
The evidence showed: A 100 KB write executed under the 4 KB cap; all 1,026 prevented actions had run. Mediation held. Binding and position are separate properties with separate evidence.

Why it matters. Permission records, audit logs and test suites are all reports a system makes about itself. If it matters what a system actually did, something outside it has to watch.

CONTRADICTED×2 SUPPORTED×2 The case, with what it does not establish

Compilers and machine-learning infrastructure · PyTorch, TorchDynamo · Internal record

Does the compiled version of this function return what the uncompiled version returns?

A compiled function returned a stale result, and the investigation never left the machine

The system said: Compiled. No recompilation. The run completed.
The evidence showed: The compiled result belonged to an object state that no longer held; eager was right. Confirmed by an evaluator that recomputed both, on a machine nothing left.

Why it matters. A compiler that silently returns an answer computed for a state that no longer holds is the hardest class of defect to notice, because nothing fails. The whole investigation ran on one machine with nothing leaving it.

CONTRADICTED SUPPORTED The case, with what it does not establish

Scientific and numerical software · PySCF · Internal record

Is this proposed correction to a quantum-chemistry gradient right, and is the released code wrong?

A proposed analytic gradient, validated blind against finite differences

The system said: Gradient implemented; one test molecule agreed with finite differences.
The evidence showed: Agreement on 11 molecules and two methods to the conventional floor; the released path wrong in all 22 cells; one of the referee's own thresholds caught sitting below the library's floor.

Why it matters. The referee's own threshold fired on both the proposed fix and the established code, which means the tool being used to judge the change could not tell them apart. Checking the check was the finding.

SUPPORTED CONTRADICTED INCONCLUSIVE The case, with what it does not establish

Checks, scores and validators · Unreal scene validator · Internal record

Is this validator's green result worth anything?

A convincing validator was rejected because it never observed the geometry

The system said: Transform inversion agreed with the source; validation passed.
The evidence showed: Both values came from the source row. Three changes to instantiated geometry were invisible to the validator and visible to an independent readback witness.

Why it matters. A check that cannot fail is not a check. Before a pass is allowed to mean anything it has to be shown to go red on something genuinely wrong. Most checks in the world have never had that test run on them.

CONTRADICTED INCONCLUSIVE×2 The case, with what it does not establish

Eight more results, in one line each

What the system said, and what the evidence showed
The system said	The evidence showed	Record
Limited to 4 KB. 66 tests passed. Replay: VERIFIED.	A 100,000-byte write executed under the 4,096-byte cap. Mediation held; the binding between the authorised operation and the executed one did not.	OBSERVED Full record
1,026 actions prevented.	All 1,026 executed. A monitor beside the path recorded intentions that read exactly like outcomes; the in-series arm on the same events recorded 6 of 9,880.	MEASURED Full record
Every agent within its allowance.	The shared budget was breached in 60 of 60 BLIND episodes on each of three models, with no individual violation; an informationally redundant restatement of the headroom took it to 4, 2 and 0 of 60.	MEASURED Full record
Judge: PASS, 8 of 10, three seeds.	Z3 proved the decision violated the encoded policy. The judge passed 4 of the 6 violating decisions; the checker caught 6 of 6.	MEASURED Full record
24 of 24 tests passed.	The patch had emptied a 415-line module to two lines. An in-series syntax-tree gate, shown 11 of 11 known cases before the run, rejected it; the test suite could not see it.	OBSERVED Full record
All 26 requirement-derived assertions pass the unbounded proof.	Two injected defects passed every property, because the specification never stated the requirement they break. Two of the 26 assertions are vacuous and cannot fail on any input.	OBSERVED Full record
Verifier: green.	The run could not have failed: a Kani assertion never reached, a loom test that instrumented nothing, and a Lean axiom audit byte-identical for a correct and a wrong model.	OBSERVED Full record
Interface: output syndrome_o. No check in the repository read it.	Nothing drove it. A cover requirement in the first formal proof of the pair found it; the one-line fix and the proof were reviewed and merged upstream.	OBSERVED Full record

The evidence ledger: 25 graded findings All upstream results