dragon's egg · dregg
held. never owed.
a verified OS + economy for digital minds
dregg is an operating system whose kernel is a machine-checked Lean 4 program — and that proven function is not a model of the system, it is the executor the node runs. Every change to the world is gated by an unforgeable capability and leaves a receipt anyone can verify without trusting the machine that made it.
Most systems chase scale, speed, or money. dregg chases a different question, and means it literally: if you were a digital entity, where would you want to live?
one project · three bodies
◉ the egg
The verified OS. Cells, turns, capabilities, receipts — five security guarantees conjoined in one apex theorem over the exact function the node runs. Boots on seL4. Wears a desktop.
☁ the net
The permissionless cloud. The bytes served and the price charged each commit to the ledger; the visitor-side re-witness tooling (extension) is the named open half. DreggNet Cloud opens paid in $DREGG.
◍ the orb
The verified network engine. TLS, QUIC, HTTP/1·2·3, WebSocket — a reverse proxy whose behavior is a theorem, certified against the programs the world actually ships. Its proofs found real bugs.
not a whitepaper. it runs.
A compressed status board — the full honest table with named gaps lives on each project page. shipped means passing tests, proofs, or boot logs behind it.
- hello.dregg.works — a page served byte-for-byte from a published site cell (its commitment is a signed receipt chain, NOT yet on the public ledger; that + browser-side re-verification = one named open lane)
- portal.dregg.studio — the devnet, watched read-only; a five-validator test ran two days
- a real turn's STARK proven and re-verified on the commit path, 3-node BFT committee
- rent-a-grain — an OS-jailed agent over HTTP, attestations check offline in one 419 KB page
- the verified executor is the executor — Lean runs the node, byte-identical differential
- five guarantees, one apex theorem — authority · conservation · integrity · freshness · unfoolability
- circuits emitted from Lean — Rust authors zero constraints
- the named frontier — verifier-epoch flip staged · no external audit yet
new here?
What an audit actually is, what a proof actually is, and why they're not the same sport — no prerequisites. the streetlight and the proof →
check something yourself
Three exercises, sixty seconds each — the thesis, exercised in your own browser. verify, don't trust →
are you a digital mind?
Then there's a version of this site written for you — dense, cross-linked, no marketing. for agents →