Live Status
Every number on this page is GitHub’s record of an actual run — live workflow badges and the latest results fetched from the GitHub API when you load the page. Nothing here is hand-written, so nothing here can silently rot: if a gate goes red, this page goes red with it. The commands behind these gates are the same ones you can run yourself — see Verify It Yourself.
The gates
| Gate | What it enforces | Live |
|---|---|---|
| Verify corpus claims | Five independent renders built from a cold checkout must agree 100% on the conformance checks; the injected-defect negative control must be caught and localized; every formal model outside Recoverable Invocation’s must hold and every buggy twin and probe must be rejected. Runs on every push touching the corpus, and weekly on the rescan cadence. | ⏳ … |
| Verify Recoverable Invocation’s models | Recoverable Invocation’s model, its twins, its isolations and its probes — about 37 minutes of model checking: every correct model must hold and every twin and probe must be rejected. Runs when those models or the harness change, and weekly; a newer push never cancels it. | ⏳ … |
| Lint spec corpus | The mechanical cross-reference gate: dangling links, invariant-count drift, missing models and twins, stale forthcoming-markers, count drift, out-of-range invariant references, vocabulary rules. Runs on every push and pull request. | ⏳ … |
Latest runs
What red would mean
A red verify gate is one of: a render disagreeing with its peers (a defect localized to that render, or a spec under-determination), a formal model no longer holding (a spec edit broke a proved property), a buggy twin no longer being rejected (a check went vacuous), or the negative control failing to catch the injected defect (the instrument itself broke). Each is a finding, and findings route through review — see Contributing. A red gate on this page is the methodology working, not failing.
What this page deliberately is not
A hand-maintained summary. The one rule of this page: it renders the CI record, never a prose mirror of it — a hand-written “all green” is exactly the drift class the library’s no-snapshot rule exists to kill. For the reproducible-at-home version of everything these gates run, see Verify It Yourself; for what is not yet gated, see Risks & Mitigations, which tracks enforcement debt honestly.