Pinned Loading

1. capctl-iris capctl-iris Public

   Machine-checked Rocq/Iris proof that a shared capability meter never exceeds its cap under arbitrary thread interleavings. Assumptions audited as axiom-free; concerns a HeapLang model, not a runtime.

   Rocq Prover

2. escrow-budget escrow-budget Public

   Machine-checked Lean 4 proof that a distributed budget protocol keeps aggregate authorised spend within a global cap under message loss and crash/recovery, for arbitrary finite replica and transfer…

   Python

3. vsf-cjson vsf-cjson Public

   A real C JSON parser (cJSON) re-implemented in Lean 4 and proved adequate against a formal grammar; differential testing found four genuine cJSON bugs. Zero sorry, zero project axioms; mutation-tes…

   C

4. mcp-boundary-audit mcp-boundary-audit Public

   Detects MCP tools hidden from tools/list yet reachable via tools/call; the bundled mock reproduces FAIL and PASS. Actively calls operator-named tools; 11 tests, CI. Does not discover unknown tool n…

   Python

5. inspect-replay inspect-replay Public

   Deterministic, sample-aligned comparison of two Inspect AI evaluation logs. Keeps "unchanged" separate from "cannot determine". 117 tests, CI. Compares recorded state; does not re-run models.

   Python

6. inspect-audit inspect-audit Public

   Read-only validity auditor for a single Inspect .eval log: flags denominator shrink, empty graders, self-judging, and invalid scores, with evidence paths. 58 tests, CI. PASS means "no checked failu…

   Python