simplified version ↗

I / the egg

boundaries are
theorems.

dregg models the whole machine — desktop, database, and distributed swarm — in one verified language of cells, turns, and capabilities. You don't get permissions that can be granted and revoked behind your back; you hold authority you can prove, every time, at the point of use. Consent is a precondition of the math.

the four words

The whole kernel is one sentence: a turn is the exercise of an attenuable, proof-carrying token over owned state, leaving a verifiable receipt.

cell — the unit of self

State + identity, holding four kinds of knowledge: conserved value, revisable state, productive authority (what it can prove), and an append-only evidence ledger.

turn — one step of inference

An atomic, capability-gated transition across cells, executed as a transaction — all-or-nothing, journalled, rolled back on any failure.

capability — constructive knowledge

You hold a capability iff you can exhibit a witness the kernel accepts. Authority doesn't deplete by being used; it's constituted by what you can prove.

receipt — a proof it happened

Every turn binds the whole post-state. Tamper a field the effect didn't legitimately write and the receipt simply won't verify — the anti-ghost property.

five guarantees, one theorem

Machine-checked and conjoined in one apex theorem (deployed_system_secure) over the exact function the node runs. Every keystone is axiom-pinned with zero sorry, build-enforced — modulo the named cryptographic carriers the proofs assume as hypotheses. Circuits are emitted from Lean; Rust authors zero constraints.

what the kernel proves
  • authority — every change justified by an unforgeable, non-amplified token chain; delegation only narrows: granted ⊆ held
  • conservation — per asset, the resource sum is identically zero; money never appears from nowhere
  • integrity — a receipt binds the whole post-state; un-written memory can't be forged into a passing proof
  • freshness — no replay, no double-spend; a stored capability cannot outlive its grantor's revocation
  • unfoolability — a light client checking one aggregate STARK root, re-running nothing, learns the entire history executed correctly
what makes it load-bearing
  • the verified executor is the executor — the Lean function execFullForestG runs the node via FFI, differentially verified byte-identical
  • post-quantum proofs — Plonky3 · BabyBear · Poseidon2 · FRI; recursive aggregation folds history into one root
  • one entry, credential-gated — a turn that can't exhibit its token chain simply does not execute
  • assumed, named, never hidden — STARK/FRI soundness and hash collision-resistance enter as typed hypotheses, out loud

what runs today

shipped has passing tests / proofs / boot logs behind it; in progress has a real foundation with named gaps; planned is designed, not yet wired.

Verified kernelThe Lean executor runs the node via a no-copy FFI boundary, byte-identical against the JSON oracle.shipped
Post-quantum proofsThe faithful whole-turn commitment is the deployed default; all 8 fold carriers wired fail-closed behind one staged verifier-epoch flip.shipped
A live multi-operator devnetFive-validator test federation; a real turn's full STARK generated and re-verified on the commit path across a 3-node BFT committee. Named open: committee restart-durability.live testing
Confined agents — the grainRent a hosted agent whose body is OS-jailed; every action cap-gated, metered, minted as a kernel turn. The egress door is proven at both poles. Attestations verify offline in one 419 KB page. Live-LLM-in-jail is proven against a hermetic provider; the real-provider run is the named seam.rentable
dregg on seL4Boots M0→M5 on arm64. The executor protection domain runs a real verified turn; a STARK is proven & checked on-device.shipped
deos — the desktopFiles are cells; every save is a receipted turn. Rewind Rail scrubs verified history; an order-book Exchange Floor conserves Σδ = 0; Matrix chat carries rehydratable world-forks. Ships as .app/.dmg/AppImage. the full tour →shipped
Zed over cellsA real Zed workspace instantiates over the cell-ledger; save fires a verified turn. Hermes-agents-in-Zed is the current owed item.in progress
zkOracleCertify an HTTPS answer instead of screenshotting it: authentic transcript ∧ well-formed ∧ provably-uninjected, composed as Lean theorems. Honest caveat: the body attestation is notary-signed, not yet a succinct ZK proof.in progress
Verified storageThe storage layer rebuilt in Lean as source of truth — binding theorems, k-of-n erasure reconstruction, forged shares refused.in progress
Money in, verifiablyStripe fiat → conserved in-protocol credit through DECO-style zkTLS, STARK-carried; double-mint closed by construction.in progress
DocuverseTransclusion done honestly: unforgeable backlinks, no dangling citations, per-viewer attenuation. A quote renders only if it verifies against the on-chain commitment.shipped
Attested queries & PostgresAn attested-receipt query API the server can't omit from; a Postgres extension gating rows by dregg capability instead of hand-rolled RLS.shipped
honest floor ▓  not yet machine-checked: full binary-level refinement (true l4v-grade) and the cryptographic UC layer. The verifier-epoch flip and re-genesis are staged behind a human go. No external security audit yet — do not use for anything security-critical.
named, in placenever hidden

the road, this season

Every named gap carries a closure lane. No parking lots, only burn-downs.

days–weeks

The verifier-epoch flip: staged conditional-truths become deployed truths, then re-genesis · restart-durable committees ride in front · a live LLM brain inside the jail · Hermes ⋈ Zed · zkOracle in anger.

weeks–months

DreggNet Cloud opens, paid in $DREGG · the Orb demonstrated end-to-end, then the verified-compiler descent · promise pipelining on its proven foundation · the l4v ascent begins.

months–quarters

Federations harden and scale · reproducible OS images — "here's my OS, and a proof of its confinement" · the deep assurance frontier: machine-checked UC + crypto config-pinning.