The protocol, in seven rungs
This is the living explanation of dregg: what the system is, taught from one sentence outward. Each rung is prose first, then the theorems and files that ground it, then a place to touch the real thing. Wherever a page states a checkable fact — the verb roster, the guarantee list, the assumption floor, the constraint grammar — the fact is embedded at build time from catalogs generated out of the verified sources, and the build fails if they drift. The prose can age; the facts cannot.
1 · The turn
The one sentence: an attenuable, proof-carrying token, exercised over owned state,
leaving a verifiable receipt. The demand⊣supply gate; the verify/find asymmetry;
atomicity.
2 · Cells & the four substances
Value is linear; authority is produced under non-forgeability; evidence is
monotone; state is guarded. The eight verbs as their structural rules — minimality
is a theorem.
3 · Guards
One predicate algebra, four polarities: caveat, program, precondition, intent. The
coordination dial (confluence-stable guards run free) and the disclosure dial
(what the proof doesn't need, it doesn't see).
4 · Receipts & Q
History as evidence: the receipt chain, the witness bundle, time-travel as a
theorem. A receipt binds the whole post-state — there is no field a tamperer can
edit.
5 · The light client
Verify everything, re-execute nothing: one check on one root learns the whole
history. The assumption floor, enumerated in full.
6 · Userspace
Factories, cell programs, and the polis: escrows and councils and constitutions as
verified cell programs. Apps inherit theorems by consuming receipts against
descriptors.
7 · The trust boundary
What is proven (the guarantees, by apex theorem), what is assumed (eight carriers),
which running code the proofs depend on, and what stays your discipline.
Above the ladder
The kernel taught here is the foundation. What stands on it: the agentic desktop, and the verified microkernel ground it boots on.
deos · the agentic desktop
A window is a capability; htmx-on-crack affordances; the rehydratable frustum-snapshot; the verified-desktop crown. dregg made visual, with zero new trust.
The firmament · dregg-on-seL4
One capability local-to-global, the
n=1 collapse to strong-local properties, the protection-domain topology that boots today, and pg-dregg verified durable state.
After the ladder
The glossary
The nine words dregg cannot be explained without — cell, turn, capability, verb, guard, receipt, Q, factory, polis — each linked to its rung.
Guides by role
Use it, build on it, run it — task-oriented references for users, developers, and operators.
The ontology catalog
Every wire effect and every predicate kind, generated from the verified sources, searchable and live.
The paper
The formal treatment: the model, the authority logic, the assurance case, the realization.