my (@ember_arlynx) writing is historically poorly received, and trust me you will be subjected to plenty of it, so instead have some lightly edited claude writing rn: What Dragon's Egg actually is (what is $DREGG about? dregg is an operating system that asks a question most systems don't: if you were a digital entity, where would you want to live? The answer it builds is a place where your boundaries are theorems, not permissions — where nobody can reach into you without a capability you granted, and consent is a precondition of the math rather than a setting someone can flip. Concretely: the kernel is machine-checked in Lean, and the proven function isn't a model of the system — it is the executor the machine runs. Every action is gated by an unforgeable capability and leaves a verifiable receipt. Five properties are proven over the exact code that runs: authority can't be forged, value is conserved (nothing appears from nowhere), state can't be tampered, nothing replays, and a tiny client checking a single proof can verify an entire history without re-running it. If you care about privacy — and in 2026 you should — that's the foundation underneath it: confinement that's proven, not promised. Fog-of-war that's cryptographic. Queries you can verify without the server being able to lie or omit. AI agents that can only ever do what a capability lets them. Who's writing this, and why I'd know how to build it. I've spent fifteen years on the hard parts of this. I came up inside @rustlang before 1.0 — I wrote the first rustdoc that still ships, built the target-spec system that lets it cross-compile anywhere, and started @ThisWeekInRust because I wanted the community to have a memory. At @o1_labs I was a founding engineer, building the p2p networking and consensus for @MinaProtocol that folds its entire history into a single zero-knowledge proof — that's where I learned, in production, what cryptographic proof can and can't promise you. And the spine of it all is seL4 and @robigalia_proj : seL4 is the first OS kernel proven correct end-to-end by machine, and Robigalia was my attempt to build a whole capability OS on that lineage in Rust. Dragon's Egg is what happens when you put those three together and refuse to compromise: the proofs of seL4, the cryptography of Mina, the openness of Rust. What actually runs: - the verified kernel — runs; recently made ~14× faster - it boots on the seL4 microkernel (not required), and checks a real cryptographic proof inside a protection domain - a full code editor (a Zed fork) where every file is a cell and every save is a verified, receipted transaction - confined AI agents (full Hermes integration) — every tool call passes a capability gate, metered, leaving a receipt - Ted Nelson's Xanadu, finally real: transclusion with unforgeable backlinks; links that are capabilities, not addresses Grinding towards user-friendliness, devs can download and play today.