Findings
Each finding is a result with an address of its own, so its independent-reproduction status can change over time and be tracked. A theorem about an artifact built to have the property is a demonstration of what is constructible, not a discovery about an existing system; the two are kept apart.
Several findings are also told as cases. One story each.
Results about existing systems
- 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.
- 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.
- 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.
- 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.
- 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.
Demonstrations of what is constructible
- 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.
- 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.
- 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.
- 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.
- 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.
- In a server built to exhibit the bug, tools filtered from the discovery listing remained reachable through the call surface: a presentation-layer authorization control with no execution-layer enforcement behind it.
- 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.
Evidence grades
- PROVEN
- Follows from stated premises inside a named frame; the frame and trusted base are always shown alongside.
- MEASURED
- Empirical, with a stated sample and method.
- OBSERVED
- Witnessed in a specific instance, with no frequency claim.
- OPEN
- A question posed and not answered.