← the landing page · the cloud & apps · this is the dense index for developers, operators, provers, and machine readers

dregg / Dragon's Egg · the technical index

a formally verified, distributed object-capability operating system. robigalia the project · dregg the kernel · deos the desktop. deos runs on dregg runs in robigalia.

The human-facing, educational site is https://www.dregg.net. This page is the dense technical index: written for LLMs, experts, and developers, organized as entry points into the repository at github.com/emberian/dregg. Every link below points at a real file at HEAD or a live surface on this site. The full dense product site (every subsystem page with its theorem names, test counts, and seam ledgers) lives at /deep/.
A turn is the exercise of an attenuable, proof-carrying token over owned state, leaving a verifiable receipt.

The kernel is a Lean 4 program with machine-checked soundness, and it is the exact function the running node executes (execFullForestG, linked via dregg-lean-ffi/). All proof circuits are emitted from proved Lean modules as byte-pinned descriptors; Rust authors zero constraint semantics. Research software: the named seams below are named, there has been no independent audit, and it is not for anything security-critical.

The model · four substances, eight verbs#

A cell is the unit of isolation and identity. Everything a cell holds is one of four substances, each with its own discipline:

The kernel signature has seven constructors, with shield and unshield as two directions of one evidence operation. The registry gives a total classification of the wire effects and proves its hand-assigned (substance, polarity) labels injective. That is a signature-level non-redundancy check, not a semantic lower bound over all possible kernels. The catalog lives in VerbRegistry.lean; queues, escrows, auctions, namespaces, councils, bridges, and channels are cell-program patterns over these verbs, not kernel primitives. A turn is an atomic, capability-gated transition across one or more cells, a forest of effects with delegation edges; delegation only attenuates (granted ≤ held). All four guard polarities (caveat, program, precondition, intent-demand) are one Pred algebra; holding a capability means being able to exhibit the witness that discharges its caveats.

The five guarantees + the running entry#

Stated as Lean theorems in AssuranceCase.lean, each pinned by #assert_axioms to exactly {propext, Classical.choice, Quot.sound}, each with non-vacuity witnesses. The reading companion is docs/reference/lean-assurance.md.

guaranteetheoremstatement
AAuthorityauthority_guarantee Every state change is justified by an unforgeable, non-amplified, fresh token chain. Production (mint) is gated on holding the issuer’s capability; the gate discriminates: it is not := True.
BConservationconservation_guarantee · conservation_guarantee_step Per asset, the resource sum is identically zero on every reachable state. Under AssetId := CellId every asset is its issuer cell; mint, burn, and fees are ordinary moves against negative-capable wells.
CIntegrityintegrity_guarantee · integrity_guarantee_whole_turn_covered A receipt binds the whole post-state; circuit and executor provably produce the same receipt. Tampering a field the effect did not legitimately touch makes the turn unprovable (anti-ghost).
DFreshnessfreshness_guarantee No replay, no double-spend: a committed spend’s nullifier was fresh (in-circuit sorted-tree non-membership), revocation takes effect at finality, and a stored capability cannot outlive its grantor’s revocation (retrieval-epoch rule).
EUnfoolabilityunfoolability_guarantee A light client checking only the aggregate root learns A–D for the entire history, re-witnessing nothing; a tampered or reordered aggregate cannot bind. Conjoins light_client_verifies_whole_history with conserves_from_verification; the anti-ghost tooth is tampered_aggregate_cannot_bind.
RRunning entryrunning_entry_sound A∧B∧C hold over execFullForestG itself (the exact gated function the deployed node invokes), not just an abstract model.
 Composed apexdeployed_system_secure ONE theorem whose conclusion is the conjunction A ∧ B ∧ C ∧ D ∧ E over one committed running-entry forest.

Assumed, named, never hidden. The cryptographic floor enters as typed hypotheses, never axiom: Poseidon2 collision-resistance, BLAKE3 CR, Ed25519 EUF-CMA, HMAC/PRF, AEAD, FRI/STARK soundness, BLS quorum certs, post-GST synchrony. Open, named. The largest open distance from l4v-grade is the deployed-binary bridge: the Lean→C/.a link correspondence and the wire-codec translation validation (dregg-lean-ffi/src/marshal.rs) are stated as obligations, not yet proven. Key-leak blast radius is bounded to the attenuation-closure of the leaked c-list (Metatheory/KeyLeak.lean). The open-obligation ledger is metatheory/CLAIMS.md § OPEN. No independent audit. Not for anything security-critical.

For LLMs and machine readers#

Dense, narration-free, file:line-grounded. Read in this order.

The reference set (docs/reference/ · Rust subsystems)

The reference set (docs/reference/ · Lean theory)

For developers#

There is no public server; everything runs from a clean checkout on localhost. The verified build needs the gitignored Lean seed archive (scripts/fetch-lean-seed.sh fetches a prebuilt one); a plain cargo build without it is the un-verified marshal-only node, which refuses to start without an explicit opt-in.

For operators#

For provers and experts#

The system itself is metatheory/ (Lean 4, library Dregg2): the eight-verb kernel, the gated executor, the circuit IR + descriptor emission, the assurance case, the deos modeling. l4v-shaped: abstract spec → executable design → refinement proofs. Build: cd metatheory && lake build.

Live demos on this site#

Every surface below is static and client-side: the verified executor is compiled to WebAssembly and runs in your tab: no backend, no account. A click is a real cap-gated verified turn against an in-tab ledger.

surfacewhat it is
/deos/ The deos cockpit (WebImage skin): cells, a moldable inspector, per-cell affordances, the ocap graph. Fire an authorized affordance → a verified turn commits, leaving a receipt in the log.
/cards/ The deos-js card gallery (counter, reflective inspector, tally board, kv-store, and doc-collab with conflicts as first-class objects), each card a real verified turn over the in-tab executor.
/explorer/ Caps-as-rows: your capabilities expressed as the rows you may read; change a token’s caveats and watch the visible rows narrow, fail-closed. The browser twin of pg-dregg’s cap-gated RLS.
/light-client/ Verify a whole finalized history in ONE recursive STARK, in-tab, re-executing nothing. Ships a real pre-folded aggregate (history.json); a tampered trust anchor is refused, not laundered. The executable counterpart of guarantee E.
/transclusion/ Xanadu made honest: a transcluded span is a verified dregg:// finalized read. Amend the source and the live quote follows; forge the bytes and the quote is refused with ContentHashMismatch; every quote leaves a receipt-pinned backlink. Verification lightens; nothing else does.
/dregg-works/ The trustless-host front door: publish = commit blake3(page) to your cell in a receipted turn; the host serves bytes it cannot alter undetected. Embeddable scripts: verify-badge.js (re-hash the served body against the on-chain commitment) and transclude.js (carry a verified dregg:// quote on any web page).
/deos-viewer/ The desktop in a link: a shared desktop is a tape (pinned instant + message sequence + claimed root), replayed through the verified executor by the reader’s own viewer; the headline is a root equality, not an image.
/atlas/ The comprehension atlas: an interactive, grounded map of the whole protocol and its UI surfaces. Source + build: docs/atlas/ (vanilla HTML/CSS/JS, no build step).
/cockpit-gpui/ The full native gpui renderer on a WebGPU canvas, driving the same in-tab executor. Heavier; present only when the gpui-web build resolved in this deploy.

The repository map#

wherewhat
metatheory/The system itself, in Lean 4 (library Dregg2): kernel, gated executor, circuit IR + descriptor emission, assurance case, deos modeling.
dregg-lean-ffi/The link: compiles the Lean executor into libdregg_lean.a and exports the entry the node calls.
node/The daemon: HTTP/MCP API, gossip + blocklace sync, block production driven by the Lean producer.
circuit/The STARK stack: the Lean-descriptor interpreter (the prover), Plonky3 (BabyBear · Poseidon2 · FRI), recursive aggregation, the light-client verifier. No hand-authored AIRs.
cell/ · cell-crypto/ · turn/ · wire/The Rust data plane: zero-crypto cell types (the four substances + programs); the crypto (notes, value-commitments, seal/stealth); turn types + executor + witness-mode/collapse; the wire codec.
blocklace/ · federation/ · captp/ · coord/The signed, equivocation-detecting, BFT-final DAG; committee machinery; capability transport (OCapN; the data plane is captp/src/data_plane.rs); coordination protocols.
dregg-doc/The document language: a Pijul-shaped patch core (changes as first-class objects, conflicts as objects, the branch-and-stitch pushout merge) plus a ropey↔patch bridge.
pg-dregg/dregg capabilities + durable verified workflows as a PostgreSQL extension (RLS + the AUTHZ → CHAIN → APPLY write spine).
starbridge-v2/ · starbridge-web-surface/deos: the native gpui cockpit embedding the real executor (src/dock/ panes, session.rs login=root-cap, powerbox.rs designate-then-attenuate) + the web-surface/affordance/rehydration stack.
deos-zed/ · deos-terminal/ · deos-matrix/ · deos-hermes/The dock apps: a code editor, a real PTY terminal, a Matrix client carrying rehydratable membranes, a ToolGateway-gated agent bridge; deos editing, building, and operating itself.
sdk/ · sdk-ts/ · sdk-py/ · cli/The three SDKs + the dregg CLI.
wasm/ · site/The in-browser executor (standalone workspace) and this site’s source (see colophon).
app-framework/ · starbridge-apps/The deos app framework + the userspace apps built on the substrate.
dregg-deploy/DreggDL, declarative deployment specs: an over-grant in a spec is caught as in-forest capability amplification before anything deploys.
sel4/The Robigalia/seL4 embedding: protection-domain crates, the Microkit assembly, the booting executor PD (the Lean kernel inside a real seL4 protection domain, under QEMU), the crypto floor. Reference: docs/reference/firmament.md.
discord-bot/Councils, real signed turns, cipherclerk macaroons; not a read-only mirror.
docs/The design documents; OVERVIEW.md is the top.

This site#

This page and every demo surface are static files assembled by scripts/build-pages-dist.sh from site/ (source layout + build knobs: site/README.md) and deployed by the manual-dispatch pages workflow, green-or-bust: a broken wasm crate fails the deploy; nothing stale ships. The wasm executors are built from wasm/ and starbridge-v2/web/ at deploy time. The human-facing, educational site is dregg.net; this index is the machine- and expert-facing half of the split, written to be read by LLMs as much as by people.