NULLIUS: a verified
object-capability substrate
A window is a capability. This note sketches the substrate that makes the claim mean something, and points at the running code that demonstrates it.
We present NULLIUS, an object-capability kernel whose entire semantics reduce to three objects — cells, turns, receipts — and whose every state change is an atomic, capability-gated, signed turn leaving a hash-chained receipt. Authority is unforgeable and attenuable but never amplifiable (a macaroon/biscuit tag chain); value is conserved by construction (mints are issuer moves); integrity is a domain-tagged commitment binding the whole post-state; freshness is a per-actor nullifier set; and a light client verifies an entire history by re-checking the receipt chain, re-executing nothing and trusting no executor. In a full deployment the executor is machine-checked in Lean, emits STARK circuits, and boots as a protection domain on the seL4 microkernel. This implementation reproduces the kernel and its light client as one executor that runs identically in a node and in the browser, and marks the formal-verification and microkernel layers as represented.
▶ Read the seven-rung walkthroughAmbient authority vs. capabilities. Why "a window is a session" is the bug and "a window is a capability" is the fix.
State behind its own program. Solvent cells, budget cells, and the enforced transition relation.
All-or-nothing commit; the signed body; per-leg guard discharge; the void-on-any-failure rule.
The HMAC tag chain; attenuation as restricting caveats; effective rights = root ∩ caveats.
Domain-tagged commitments, prevHash pinning, monotone sequence, unfoolability against the pale ghost.
One capability across a distance parameter; the n=1 collapse to strong-local; the substrate on seL4.