The protocol,
in seven rungs
One sentence unfolding outward: a turn is the exercise of an attenuable, proof-carrying token over owned state, leaving a verifiable receipt. Each rung expands one clause of it.
1 · The turn
A turn is an atomic batch of actions signed by an actor. It is the only way state changes. It commits entirely or not at all: a forged credential, an overdraft, or a stale nonce on any leg voids the whole turn and leaves the state untouched.
2 · The substances and the verbs
State lives in cells: each holds balances, capability slots, named slots, and a predicate over its own transitions. The reference verbs are transfer (move value, conserving it) and set_slot (write a named slot). Each action presents a capability — a token naming what it may touch and how.
3 · Guards
A guard is a condition the turn must discharge. Two do most of the work: the authority guard (required ⊆ held: the presented capability must actually grant the verb after its caveats narrow it) and the predicate guard (the target cell's program must accept the transition — a solvent cell refuses to go negative; a budget cell refuses to exceed its lifetime limit).
4 · Receipts
A committed turn leaves Q — a receipt binding the entire post-state via a domain-tagged commitment, with no field a tamperer can edit. Receipts chain: each pins its parent by hash, so reorder, drop, or insert is detectable. The receipts are the history; scrubbing them backward is time travel, which is what the explorer does.
5 · The light client
A stranger runs the smallest possible check and learns the truth about the whole history. verifyHistory(receipts) re-checks each commitment opens, each prevHash pins its parent, and the sequence is monotonic — re-executing nothing and trusting no executor. A server presenting a plausible state it never legitimately produced — the pale ghost — cannot pass, because there is no valid chain for a forged history.
6 · Userspace
Above the kernel, apps are sets of cells exposing affordances rendered as surfaces (see Surface). A line of credit is an attenuated capability; an encrypted group is a cell whose membership is physics; a game's fog of war is the membrane's per-viewer projection. Each is an SDK noun riding the same executor — no new kernel entry.
7 · The trust boundary
What must you trust? The cryptographic floor (ed25519, HMAC, a collision-resistant commitment) and, in a full deployment, the Lean kernel's three axioms plus a real STARK on seL4. NULLIUS enforces rungs 1–5 in running code and represents the formal-methods and microkernel layers — stated plainly on the Verify page. Trust is something you check, never something the page claims.