simplified version ↗

deos / the desktop

a window is
a capability.

deos is dregg made visual, interactive, and webby — with zero new trust. Every visual primitive reduces to a kernel theorem: a window is a capability, an interaction is a verified turn, a screenshot can be a living membrane. It's not an app on the verified OS; it's what the verified OS looks like.

see live renders the cockpit source

four theorems, worn as furniture

The verified-desktop claims aren't vibes — each is a discharged Lean theorem the surfaces merely wear.

login is a capability

No auth subsystem, no session table. Logging in is receiving your root capability; a session is the cap-tree you hold; logout is revoking it — and the whole desktop darkens synchronously. Your world reopens exactly where you left it.

the powerbox

The "open file dialog," reimagined as a grant ceremony: a confined app asks for authority it lacks, you pick from only what you actually hold, and a fresh attenuated capability is minted by a real turn. Designate, then hand over strictly less than you have.

the rewind rail

A time-travel scrubber above the taskbar. Drag it and the desktop re-derives at any past moment by verified replay of the receipt chain — the past is read-only, and the live world is never touched. The desktop scrubs its own history like a video.

the living screenshot

A deos "screenshot" embeds a sturdyref behind a membrane: opening the image re-attaches a live, per-viewer, attenuated surface, confined by construction. A forwarded view can never amplify — that's a theorem, not a policy.

what's on the desk

Documents with real patch theoryVersion control is the document: edits are patches, merge is a provably-sound pushout, and a conflict is a first-class object you live in — never a silent overwrite. Blame survives moves.shipped
Matrix chat with membranesA native Matrix client (real E2EE; any Matrix client can join the room) where a message can carry a cap-bounded fork of your world — the recipient rehydrates it, drives real turns, and stitches back.behind a flag
The Exchange FloorA desktop window for the agent economy: an offer is a fresh cell, post → lease → settle are each real turns leaving receipts, and value conserves Σδ = 0 across the book.shipped
Hermes — the agent in the sidebarA real tool-calling LLM agent where every tool call is cap-gated, budget-metered, and receipted — or refused in-band, naming the exact mandate that bit. Budget bars deplete live on screen.behind a flag
Zed over the ledgerA real code editor pane where saves are verified turns. The full variant backs Zed's git stack with the cell ledger — each save a commit, blame from the patch chain — and is honest about its seams: it passes standalone, isn't wired into the cockpit yet.in progress
The MUDA multi-user text world where the security proofs are the game rules: a room is a cell, an item is a capability (duping is inexpressible), a locked door is a cap you lack. The fog-of-war is fail-closed — you provably cannot even prove the enemy's vision.first slice
Web-deosThe real verified executor compiles to wasm and runs in your tab — a button click commits a real turn and the page repaints from the committed ledger. Live card pages (counter, kv-store, collaborative doc with pushout merge) exist; the full web cockpit has painted its first frame and is honestly WIP.cards real; cockpit WIP
The dockSplit, resize, tear off, float — a full pane workspace whose surfaces are capability-holding objects that migrate between panes. Inspector, world explorer, transcript, workflow composer, mail room, app shelf.shipped

Everything above is reproducible: the repo carries a runbook where each entry is a copy-paste command that hard-asserts its own proof — including the self-hosting loop, where an editor save is a receipted ledger turn and a live terminal compiles that very edit, inside deos.

designed, said plainly

Two directions on the drafting table — design docs in the repo, not shipped surfaces. Named here because the substrate for both already runs.

the dregg-native forge

A code forge with no git anywhere: the patch theory is the version control. A repo is a cell, a commit is a receipted turn, history is unforgeable (you cannot rewrite someone's blame), and CI needs no trusted runner — the proof is the pass. The engine exists; the product surface is the design.

the grain-homeserver

Today the Matrix membrane rides an external homeserver — the one piece of the distributed desktop not dregg-hosted. The design: run the homeserver itself as a confined, metered, receipt-audited grain. dregg hosts its own membrane; any Matrix client still joins.

honest floor ▓  the four keystone theorems are discharged; the rich dev panes (editor, terminal, chat, agent) ship behind a feature flag while they harden; the web cockpit is a first frame, not a daily driver. Ships as .app/.dmg/AppImage — a heavy build; use --release.
zero new trustproofs as furniture