Projects
Each artifact explains one question, its method, its result and its limits. Maturity is labelled honestly; most are research prototypes.
Formal verification
| Project | What it establishes | Maturity | Grade |
|---|---|---|---|
| escrow-budget | A budget bound (spend within cap) holds for all reachable states, machine-checked. | research prototype | PROVEN |
| vsf-cjson | Four kernel-checked theorems about a JSON parser and serialiser, with a differential over 120,000 inputs. | research prototype | PROVEN |
Agent control
| Project | What it establishes | Maturity | Grade |
|---|---|---|---|
| mcp-authority-boundary | Mediation held; binding did not. | research prototype | OBSERVED |
| capctl-iris | A concurrent capability bound holds over every interleaving, machine-checked with no axioms. | research prototype | PROVEN |
| safeguards-control-plane | A monitor reports intentions as outcomes. | research prototype | MEASURED |
| compositional-temporal-safety | A compositional safety invariant holds for all finite N, machine-checked. | research prototype | PROVEN |
Evaluation integrity
| Project | What it establishes | Maturity | Grade |
|---|---|---|---|
| evaltrust | Two off-the-shelf LLM judges fail in opposite directions; a zero-disagreement judge's agreement interval is degenerate. | research prototype | MEASURED |
| inspect-replay | Two evaluation logs compared deterministically, distinguishing 'unchanged' from 'cannot tell'. | research prototype | MEASURED |
| inspect-audit | A read-only auditor flags silent validity failures in evaluation logs. | research prototype | MEASURED |
Security engineering
| Project | What it establishes | Maturity | Grade |
|---|---|---|---|
| escrow-budget-mpst | The transfer session is deadlock-free and crash-safe by typing; the budget bound is not expressible in it. | research prototype | PROVEN |
| mcp-boundary-audit | A harness detects a tool hidden from discovery yet reachable through the call surface, on a mock built to show it. | research prototype | OBSERVED |
| semdiff | A deterministic, severity-ranked semantic diff for four high-risk engineering formats, no LLM calls. | research prototype | MEASURED |
Assurance architecture
| Project | What it establishes | Maturity | Grade |
|---|---|---|---|
| OMEGA | A sealed, replayable decision record whose tamper-evidence is machine-checked. | research prototype | PROVEN |
| nanogpt-provenance | A verifier re-derives a training run bit-for-bit; cross-hardware re-derivation stays UNKNOWN, not claimed. | research prototype | MEASURED |
Upstream contributions (proposed)
Changes proposed to verification projects maintained by others. Each is an open pull request under review. None has been merged, and none is claimed here as an accepted contribution; each link shows the current state, checked on 2026-08-06.
| Project | Proposed change | Status |
|---|---|---|
| cedar-policy/cedar-spec #995 | A differential-testing target comparing the typed expression produced by the Rust and Lean typecheckers, against upstream issue #840. | Open, changes requested |
| strata-org/Strata #1448 | Classify bugFinding goals with the mode-aware predicates at the minimal check level. | Open |
| strata-org/Strata-CLI #7 | Count verification goals with the predicate that matches the check mode. | Open |
| strata-org/Strata-CLI #8 | Bump lake-manifest.json to a Strata revision that StrataMainLib compiles against. | Open |