deos — the agentic desktop
deos is the userlayer of robigalia: everything a human or AI agent
touches. It is dregg made visual, interactive, and webby — with
zero new trust. The realization underneath it is simple and total: the web's
interaction model is the right way to build a desktop, and a capability substrate can
make every piece of it gated, verified, and attenuable instead of ambient-authority
soup. A window is not a thing a session lets you see — a window is a
Capability{ Surface(cell), rights }.
So: deos runs on dregg runs in robigalia. Nothing in deos adds authority the kernel does not already prove. The desktop's safety is not a new system to audit; it is the kernel's own metatheory, restated for pixels, affordances, and rehydration.
htmx on crack: every element is a verified turn
In htmx, an element declares hx-post="/x" and the server returns a fragment.
That declarative, server-rendered, progressively-enhanced model is the right UX. deos
keeps it and changes what each piece means:
A cap-gated affordance
A cell declares affordances: named, typed effect-templates. The "button" is one of them — a real Effect the cell offers, not a route the server interprets by convention. An affordance carries the genuine effect; whether it may fire at all is decided in-band by the proven gate.
Held capabilities, not a cookie
An affordance renders and fires only when required ⊆ held — the genuine is_attenuation check, the same proven lattice the kernel uses, never a new gate. Progressive enhancement becomes progressive attenuation: an agent sees exactly the affordances its capabilities authorize, and two viewers diverge over one surface.
An attested post-state surface
Firing an authorized affordance yields a verified-turn intent; the returned surface is the attested post-state. An unauthorized fire is refused in-band — the anti-ghost tooth. Every interactive element is a turn the witness-graph records, so there is no UI claim the system did not actually produce.
This is steel today in starbridge-web-surface: a CellAffordance
is a named dregg_turn::Effect template, the render/fire gate is the genuine
is_attenuation, and project_for returns the per-viewer
affordance set. The one remaining seam is dispatching a fired affordance to a live
TurnExecutor — the same serve-turn seam the web-of-cells fetch names; the
effect carried is the real one.
A screenshot you can re-open, live
This is the truest thing deos offers that nothing else can — not a feature port, a category only this substrate can have. A deos "screenshot" is a frame of the certified compositor over the witness-graph, and what it actually embeds is a sturdyref behind a membrane. Opening the image re-attaches a live — or faithfully replayed — interactive surface, shaped by who you are and what you hold.
Faithful by where it came from, not by retrofit
The naive version embeds a faithfulness proof in a PNG and asks a viewer to instantiate arbitrary author-state — an attack surface, not a feature. deos moves the proof upstream and structural: the frame came out of a compositor whose render pass is itself a verified turn over the witness-graph, so it can only draw what the graph authorizes. "Faithful" stops being a property you prove about an image and becomes a property of where the image came from. The screenshot rehydrates because it was never a dead artifact — it is a paused camera on a running, witnessed scene.
Per-viewer, attenuated, revocable
A plain sturdyref reconnects you to the thing. A membrane-mediated one reconnects you to a view of the thing shaped by your authority. Two agents opening the same snapshot rehydrate two different surfaces — each negotiates, across the membrane, the slice their capabilities authorize. The frustum is re-derived per-viewer from (their authority) ∧ (the graph's permitted projections). "I shared a screenshot" stops being "I leaked my session" and becomes "I extended a revocable, attenuated, per-viewer right to re-view." A reshare chain A→B→C composes through the real is_attenuation; an amplifying hop is refused.
The liveness cost is a type, not a promise
If the contexts are gone, the membrane replays from the witness-graph — and replay is only as faithful as the graph was deterministic. deos cannot wave that away, so it types it: every rehydration is Live, ReplayedDeterministic, or ReconstructedApproximate. The type is derived, not hand-set: a context whose every external interaction was an attested turn replays deterministically by construction; a context that reached outside the membrane is intrinsically approximate, because the thing that made it non-deterministic was never witnessed. Opening the image tells you which kind of true you are getting.
The unit of portability was never the data or the connection — it is the revocable
right to renegotiate the connection, which is exactly a sturdyref behind a membrane.
The sturdyref encoding, the membrane enforcer (per-viewer projection + the
chained-attenuation algebra over the real is_attenuation), and the derived
liveness-type are running, tested code in starbridge-web-surface; the
certified compositor-PD and the libservo link are the frontier.
The membrane is a settings page you already understand
The membrane's negotiation semantics are not an exotic new protocol — a GitHub organization's settings page already is a membrane UI. Teams are capability groups; repo roles (read / triage / write / maintain / admin) are the attenuation lattice; visibility is projection scope; fork policy is the re-share rule; member management is grant and revoke; branch protection is the constraint set on permitted actions. Every membrane primitive has a boring, familiar home there — and a settings page is itself a rendered view over the org's permission graph, the same kind of object as the thing it governs. Familiar UX is what makes deos adoptable; the capability-plus-proof substrate is what makes it sound.
A game where the mechanic is the security property
The sharpest exemplar of deos is a multiplayer game, because the deos novelty is a game mechanic made into a security property. What a player can see is exactly what its capabilities authorize it to rehydrate — fog of war as a cap-confinement property, not a client-side visibility flag. It runs today (two demos, agent-vs-agent matches to a decision), built on the genuine cap discipline.
Fog = the membrane projection, proof-backed
Two players' identities are incomparable capabilities — neither attenuates the other — so a tile gated to the enemy is structurally un-projectable. And the vision predicate is a real proof obligation: to project a side's tiles you must produce a proof the registry verifies. A player holding only its own secret literally cannot construct the enemy's vision, and a forged proof is rejected. Fog stops being honor-system and becomes a confinement theorem with cryptographic teeth.
Moves are cap-gated verified turns
A move is a real affordance firing a real effect; claiming an objective is another. Terrain occludes line-of-sight — a unit's vision is a cone the terrain carves, not a uniform disc. An unauthorized fire (Red firing Blue's move) is a refused turn through the same is_attenuation gate, in-band. There is no separate anti-cheat system because the cheat is unrepresentable.
A smarter brain does not get a bigger cage
An AI agent-player fires the same cap-gated affordances a human does; its action space is its attenuated capability set. A better policy only ranks within the fixed action set — it cannot cheat any more than a human can. Two agents play a full match to a win condition entirely through the gate, every action a real fired affordance. This is what "agentic desktop" means.
Multiplayer is the web-of-cells (each player a cell, the board a shared cell), a peer reaches a world by a verified attested read, and spectating is the membrane as a negotiation surface — a player proposes an attenuated spectator grant (watch-my-side / scoreboard-only / full-board-post-game), minted only as a genuine attenuation of what they hold, fog-respecting and liveness-typed. It is htmx on crack you can play, secure by construction.
The desktop adds no trust — and that is a theorem
Because deos adds zero new authority, its safety is provable from the kernel's own
metatheory. None of these is new mathematics — each is the firmament's existing proof
(attenuation, the gate, the receipt chain, unfoolability) restated for the desktop. The
modeling lives in metatheory/Dregg2/Deos/:
Surface(cell) is a point on the existing (target, rights) gradation — the same shape as the kernel's "this cap confers no extra edge" theorem.
is_attenuation across hops: reshare A→B→C means C's authority ⊆ B's held ⊆ A's. The membrane cannot amplify — the proven lattice law, lifted to projection composition.
ReplayedDeterministic is exactly the confined fragment — a context whose every external interaction was an attested turn — otherwise ReconstructedApproximate. The "type it" discipline, lifted to a theorem.
Built, queued, and frontier
The deos UI substrate, running
In starbridge-web-surface: the cap-confined web surface delegate, the dregg:// web-of-cells attested fetch, the rehydration stack (sturdyref, membrane enforcer, derived liveness-type), the cell-affordances + frustum-snapshot layer, and the fog-of-war world with its proof-backed vision and agent players. Runnable demos, tested.
The Lean modeling + the live wiring
The four verified-deos theorems above; the membrane wired into the live CapTP sturdyref path (not just the web crate); the native cockpit embedding the affordance surfaces; the app-framework composed into a one-afternoon dregg new deos-app scaffold over pg-dregg durable state.
The real pixels
The certified compositor protection-domain — the sole framebuffer-and-input capability holder on seL4 — and the libservo link. Today a dregg:// attested fetch stands in for the compositor's render pass. The firmament is the ground it lands on.
Keep going
n=1 collapse, what boots today.
Build a deos app
Cells exposing affordances, rendered as surfaces, over verified state. The factory vocabulary, the worked examples, the first-app tutorial.
The kernel, in seven rungs
What dregg is under deos — turns, substances, guards, receipts, the light client, the trust boundary.
What is proven
The five guarantees, ARGUS and unfoolability, the assumption floor, the honest seams — and how to check it yourself.