PROVEN
capctl-iris
A concurrent capability bound holds over every interleaving, machine-checked with no axioms.
§ 7.3
Artifacts
19 repositories. Each states what it establishes, what it does not, what has to be trusted for the result to stand, and the command that reproduces it.
PROVEN
compositional-temporal-safety
A compositional safety invariant holds for all finite N, machine-checked.
PROVEN
escrow-budget-mpst
The transfer session is deadlock-free and crash-safe by typing; the budget bound is not expressible in it.
PROVEN
escrow-budget
A budget bound (spend within cap) holds for all reachable states, machine-checked.
MEASURED
evaltrust
Two off-the-shelf LLM judges fail in opposite directions; a zero-disagreement judge's agreement interval is degenerate.
MEASURED
inspect-audit
A read-only auditor flags silent validity failures in evaluation logs.
MEASURED
inspect-replay
Two evaluation logs compared deterministically, distinguishing 'unchanged' from 'cannot tell'.
OBSERVED
mcp-authority-boundary
Mediation held; binding did not.
OBSERVED
mcp-boundary-audit
A harness detects a tool hidden from discovery yet reachable through the call surface, on a mock built to show it.
MEASURED
nanogpt-provenance
A verifier re-derives a training run bit-for-bit; cross-hardware re-derivation stays UNKNOWN, not claimed.
PROVEN
OMEGA
A sealed, replayable decision record whose tamper-evidence is machine-checked.
MEASURED
safeguards-control-plane
A monitor reports intentions as outcomes.
MEASURED
semdiff
A deterministic, severity-ranked semantic diff for four high-risk engineering formats, no LLM calls.
PROVEN
vsf-cjson
Four kernel-checked theorems about a JSON parser and serialiser, with a differential over 120,000 inputs.
MEASURED
commons-agent-lab
A pre-registered study of whether LLM agents produce the collective failure that per-agent rules permit.
MEASURED
proof-carrying-evals
Governance properties routed to the checker whose logic fits, with the LLM judge's score sealed beside the proof.
OBSERVED
spcu-verification
A small power-control IP verified with open tools; two injected defects invisible to every specification-derived property.
OBSERVED
evidence-audit
A grader for recorded verification outputs that reports what a run explored, not the verdict it printed.
PROVEN
collective-bound
The formal core behind the collective-bound result: Lean 4 (six theorems, no axioms), Z3 (eleven sealed verdicts), a learning adversary, negative controls.