*Part 8 of An OS Where the AI Is Never a Principal.*
The previous post ended on a claim I want to honour here: safety is model-independent. The membrane decides; the model only proposes. A grammar-constrained local model and a frontier model over a gateway both come out the same on the far side of the gate — confined.
But there is a deputy I have been quietly trusting this whole time, and it is time to name it.
When an agent calls a tool, *something runs that tool's code.* If the tool is untrusted — and in this world everything the model can reach is untrusted — then the thing that runs it is a confinement, and the strength of that confinement is the strength of your whole story. The capability says "you may invoke this tool and nothing else." The isolation says "and when you do, the code cannot climb out of its box." Both have to hold.
This post is about that second half. The same untrusted tool, confined six ways, each wrapped as the *same* Aegis capability — and what changes as you climb.
The shape that doesn't change
Here is the trick that makes the whole ladder legible: from the membrane's point of view, every rung is identical.
const tool = makeProcessTool(...) // or docker, gvisor, microvm, firecracker, sel4
const cap = wrapAsCapability(tool) // a typed cap, no ambient authorityThe tool runs somewhere — a child process, a container, a guest kernel, a verified protection domain — and the agent reaches it the only way it can reach anything: through an unforgeable reference. It shares no memory with the parent. It holds none of the parent's caps. Its output comes back labeled by provenance. Kill it and the capability is severed. The substrate doc calls this the *isolation plane*, and its rule is "a tool is a capability" — true at the type level, true regardless of what's behind the type.
So the ladder is not six different security models. It is one security model, asking one question at six different volumes: how hard is it for the confined code to escape the box you put it in?
Every demo runs. pnpm demo:isolation, demo:docker, demo:gvisor, demo:microvm, demo:firecracker, demo:sel4. They run live where the host supports the mechanism and skip the live boot otherwise — so the suite stays green whether or not your laptop has KVM. I ran all of them, on a laptop, through WSL2. Hold that fact; I'll be honest about what it costs us at the end.
The mechanism rungs — stronger, all unverified
Bare process (`demo:isolation`). The weakest rung. The tool runs in its own OS process: separate address space, separate cap set, output labeled by provenance, killable. That already buys a lot — no shared memory, no inherited authority. But it shares the host kernel. Every syscall the tool makes goes straight to the same Linux kernel running everything else. A kernel bug is a way out.
Hardened container (`demo:docker`). A container is the same process with the kernel's namespaces and cgroups drawn tightly around it. The demo runs the tool with --cap-drop=ALL --network=none --read-only --security-opt=no-new-privileges plus pid and memory limits. The line that matters: with no network, the tool's *only* channel back to the world is the capability. That is the ocap discipline and the OS sandbox saying the same thing. But it is still the host kernel underneath — namespaces are a kernel feature, and the syscall surface is the whole attack surface.
gVisor (`demo:gvisor`). Here the surface shrinks for real. gVisor's runsc is a userspace kernel: it intercepts the tool's syscalls and services them itself, so the tool almost never touches the host Linux kernel directly. The demo runs it standalone (runsc do, no Docker daemon), network off, wrapped as a cap, output labeled isolated-gvisor. You've traded a sliver of compatibility for a dramatically smaller host kernel attack surface — without paying for a full VM.
microVM via KVM (`demo:microvm`). Now the tool gets its own guest kernel, hardware-isolated by KVM. No network, no disk, no shared filesystem; the serial console is its only channel. The escape problem changes character: the code is no longer trying to find a hole in a shared kernel — it's trying to break a hardware virtualization boundary. The microVM was built with zero downloads: a static-C init, a python-packed initramfs, and the reused WSL2 kernel. The QEMU rung.
Firecracker (`demo:firecracker`). The same hardware-virtualization isolation as the QEMU microVM, but via Firecracker — the minimal VMM that AWS Lambda runs on. The tool boots as PID 1 in a stripped guest, request in over the kernel cmdline, response out over the console, a *fresh microVM per call*. Same isolation as the rung below, but the VMM is production-shaped and the boot is minimal. This is the strongest *unverified* rung.
Notice the arc. From process to Firecracker, every step shrinks the surface the confined code can attack — from "the entire host kernel" down to "a hardened hardware-virtualization boundary." But read that sentence again and the word doing all the work is *shrinks*. None of it is proven. Each mechanism is strong, and each mechanism has had bugs, and a bug in the mechanism is an escape. You are buying smaller attack surfaces with no guarantee that the remaining surface is sound.
The assurance rung — a different kind of thing
Then there is seL4, and it is not a louder version of the question. It is a different question.
mechanism ladder: process < container < gVisor < microVM (KVM) — stronger isolation, all UNVERIFIED
assurance: < seL4 — PROVEN isolation (separation kernel)seL4 is a formally-verified microkernel: it carries machine-checked mathematical proofs that its isolation properties actually hold — not "we fuzzed it hard," but "we proved it." On demo:sel4 the untrusted tool runs as a confined Microkit *protection domain* on the verified kernel, booted on qemu-aarch64, output labeled isolated-sel4-verified. A fresh image is built and booted per call.
The difference is categorical. Every rung below says *we tried very hard and found no escape.* seL4 says *there is a proof that this class of escape cannot occur.* Confinement stops being strong and becomes proven. That is ADR 0001's optional phase-3 verified floor, and the irreducible-limits doc's answer to "something must be trusted": you cannot reach zero TCB, but you *can* make the kernel under everything a thing whose isolation is machine-checked rather than merely tested.
This rung descends directly from the work of Gerwin Klein, Gernot Heiser, and the team at Data61/UNSW — and it sits in a longer lineage the whole ladder borrows from: Capsicum's capability mode, Genode and Fuchsia/Zircon as capability-structured OSes, WASI as a capability-oriented component sandbox. None of it is mine. The contribution here is narrow: wrapping each as the *same* Aegis capability so you can climb the ladder without changing the agent above it.
The honesty tax
I would be doing exactly the thing this series argues against if I let "it runs on the verified microkernel" land without the caveats. Three of them, all load-bearing.
It all ran inside WSL2-on-Windows. That is a long trust chain — Windows under a Linux VM under emulation — and it is *dev-grade*, a demonstration of each rung, not a hardened deployment. The real target, per ADR 0001, is a Linux box with direct KVM and, if you ever take phase 3, seL4 on real hardware. What I have shown is that the rungs *exist and run*, reached identically; not that this laptop is a production substrate.
The seL4 proof covers the kernel, not our code. This is the one people most want to overclaim. seL4's theorems are about the *microkernel's* isolation. Our protection domain, the Microkit tooling, the control plane standing on top — all unverified. And we used the *prebuilt* SDK under QEMU, not a from-source rebuild with the proofs re-checked. seL4 gives a proven *floor*; it says nothing about the things standing on it. A proven floor under an unproven house is still progress — but call it what it is.
The model is never on the verified floor. This is the point of the substrate decision, not a gap in it. Inference is a multi-gigabyte blob of opaque GPU code; it cannot live in a small verifiable base and you would never want it to. So inference is reached *as a capability*, always — a confined Linux guest behind a cap-routed channel, never part of the trusted base. Even with seL4 underneath, the "verified OS" contains a big *unverified* Linux guest doing inference. That is not embarrassing; it is the design. Verification proves *everything else is isolated from that guest.* It's also why CPU is the guaranteed inference floor — CPU inference pulls no GPU driver into the base, which is the only reason the verified path stays reachable at all.
Why a ladder and not a winner
You might expect the conclusion to be "use seL4, problem solved." It isn't, and the reason is the whole point of having a ladder.
The mechanism rungs trade isolation strength against cost, compatibility, and boot latency — a bare process is instant and weak; a fresh Firecracker per call is heavier and strong. The assurance rung trades *everything* for a proof, and you adopt it, as ADR 0001 puts it, only if a verified isolation floor is the product's reason to exist. Steps one and two give roughly ninety percent of the security at ten percent of the cost. Step three is for when the pitch is literally "verified AI confinement."
What stays constant up the entire ladder is the capability. The agent above never learns which rung it's standing on. You can move the floor from a process to a verified microkernel and not touch a line of the membrane — because the membrane was never trusting the isolation to be *strong*. It was trusting it to be *there*, behind a reference the model cannot forge.
The model proposes. The capability disposes. And underneath the capability, you get to choose exactly how proven the box is. That choice is the ladder.
The next post leaves the metal behind and shows the idea generalizing somewhere unexpected: an ordinary microblog turns out to be a capability system wearing ACL clothes — sharing is delegation, visibility is information-flow, and the social graph *is* the capability graph. If you want the machinery underneath all of this spelled out from first principles, the older Endo and Agoric tutorial series is the companion to this one.
End of Transmission.