agentOS

agentOS is a bootable, capability-secured I/O and isolation platform on the seL4 microkernel. It owns devices in user mode and hosts Linux and FreeBSD as virtio guests. QEMU is the hardware emulator used for prototyping; the same driver PDs that own QEMU's virtio devices today are meant to own real devices on a board.

• seL4 is the only kernel-mode code (EL2 on AArch64). It is never modified.
• The root task (kernel/agentos-root-task/) distributes untyped memory, CSpaces, VSpaces, and initial capabilities to a fixed set of protection domains (PDs), then parks. It enforces no policy after spawn.
• Driver PDs own exactly one device class each: a device frame plus its IRQ. Nothing else maps that frame.
• Virtualizer PDs own no device. They are the only multiplexer for a class, moving data between clients over sDDF-shaped shared-memory queues with seL4 notifications, and speaking the driver's contract on the clients' behalf.
• VMM PDs run a vCPU and vGIC and emulate virtio-mmio net, block, and console devices for a guest, using libvmm. Guests run unmodified in-tree virtio drivers. Guests never see host MMIO.
• Native agents are clients of the virtualizers, the same as a VMM backend. They are not in the trusted computing base.

 Hardware / QEMU
      |
 seL4 (EL2)
   |-- root task
   |-- driver PDs        serial_pd, net_pd, virtio_blk (+ block_pd)
   |-- virtualizer PDs   net_virt, blk_virt         (console: still a library)
   |-- guest_vmm_*       vCPU + vGIC + emulated virtio-net/blk/console
   |     |-- Linux guest
   |     '-- FreeBSD guest
   '-- control           vm_manager, cc_pd, nameserver, log_drain, fault_handler

The binding description of the trust boundary, with a strict split between what boots today and the target shape, is docs/TCB.md. The project rules are CLAUDE.md and AGENTS.md.

The default AArch64 image boots 13 PDs. The list is checked in two places that must agree: kernel/agentos-root-task/src/system_desc_aarch64.c (what the root task spawns) and kernel/agentos-root-task/agentos.toml (what is bundled into the image). A bundle entry with no descriptor row is never started; a descriptor row with no bundle entry fails at ELF load.

guest_vmm_secondary, fault_inject, test_runner, and event_bus are added only to the image variants that use them (dual-guest, fault-injection, and TAP test images). The other sources under kernel/agentos-root-task/src/ and services/ are still compiled so they keep building, but they are not in the image; docs/TCB.md lists them as museum code that must not be extended.

Full walkthrough: docs/QUICKSTART.md. Short form:

Host packages (the Makefile does not install these):

# macOS
brew install llvm lld qemu dtc libarchive zstd cmake ninja coreutils
# Debian/Ubuntu
sudo apt-get install -y clang lld llvm qemu-system-arm qemu-system-x86 \
    device-tree-compiler libarchive-tools zstd cmake ninja-build curl
# Rust (stable)
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y

Then:

make setup                     # build xtask, download Microkit SDK 2.1.0, check tools
make build TARGET_ARCH=aarch64 GUEST_OS=none
make test  TARGET_ARCH=aarch64 GUEST_OS=none   # boot in QEMU, wait for "agentOS boot complete"
make test-host                 # host-only suite + policy check + source lint
make test-inspect              # real boot snapshot through CC and agentctl
make test-inspect-readonly     # seL4 rejects a CC write to the snapshot page
make test-log-rings            # native generic logs through isolated rings and UART
make test-log-isolation        # native ring-region/configuration access faults
make test-operator-session     # native text protocol through serial_virt
make test-guest-net            # Buildroot: one frame through emulated virtio-net
make test-guest-blk            # Buildroot: one request through emulated virtio-blk
make test-guest-console        # Ubuntu initramfs: login over emulated virtio-console
make gate                      # the OS-claim gate: all of the above plus x86_64 boot

The Microkit SDK lands in $HOME/.cache/agentos/microkit-sdk-2.1.0 unless SEL4_SDK points elsewhere. QEMU logs and control sockets go to build/tmp/; set AGENTOS_TMP_DIR to a short path when the checkout path is long (macOS caps Unix socket paths at 104 bytes). make help lists every target.

For a running AArch64 image, build with make -C tools/agentctl and run tools/agentctl/agentctl --socket PATH inspect using its control socket. The structured report describes boot observations; current thread state is unknown and memory usage is an accounted-page lower bound. The CC socket remains a privileged control channel; inspect is a read-only operation, not a separate read-only credential. tools/agentctl/agentctl --socket PATH session-inspect obtains the same report through a separate native serial client. It uses a single serialized stream: inspect.snapshot returns ok N followed by exactly N report bytes. There is no interactive shell or mutation command in this protocol.

The dual-guest demonstration (make demo, make demo-test) boots Ubuntu and FreeBSD concurrently and proves key-only SSH to both. See docs/demo.md. It downloads two ISOs of about 4 GB each and runs for a long time under TCG.

kernel/agentos-root-task/     root task, booted PD sources, IPC contracts
  src/main.c                  boot: parse image, spawn PDs, map regions, park
  src/system_desc_aarch64.c   compile-time PD descriptor table (pd_desc_t)
  agentos.toml                PD bundle manifest (must match the descriptor)
  include/contracts/          packed-struct IPC contracts, one header per PD
kernel/loader/                seL4 loader
platform/                     shared I/O platform
  include/platform/           sDDF-shaped queue layouts (net, blk, serial), GPA translation
  net-virt/                   net_virt PD, hub/loopback pump, VMM virtio-net glue
  blk-virt/                   blk_virt PD, RAM-disk pump, VMM virtio-blk glue
  serial-virt/                VMM virtio-console glue (library, not yet a PD)
  guest-vmm/ guest-ram/       guest-neutral VMM runtime, bounds-checked GPA->HVA
libvmm/                       vendored libvmm (UNSW): vCPU, vGIC, virtio device models
services/                     driver PD sources: net-service (net_pd), serial-mux (serial_pd), vibe-engine
guest-profiles/               versioned TOML guest personalities (buildroot, ubuntu, freebsd, ...)
guest-scenarios/              multi-guest compositions (dual-release.toml)
boards/                       per-board build config (qemu-aarch64, qemu-x86_64, rpi5, intel-nuc, ...)
xtask/                        Rust task runner: build image, QEMU tests, guest fetch, release
tests/                        host suites, source lint, guest-path tests, e2e scripts
tools/                        agentctl and Rust generators (gen-abi, gen-sdf, sign-wasm, ...)
skills/                       text-only operating notes per block (sel4-platform, sddf-net, ...)
docs/                         TCB.md, ROADMAP.md, RELEASES.md, guides; see docs/README.md

contracts/, userspace/, libs/rust-pd, examples/, and manifests/ hold host-side models, simulation crates, and older agent-facing contract drafts. None of them runs on the booted target.

Host tests stub seL4 IPC and cannot be cited as proof of I/O. Only a booted image asserted by an automated QEMU test can.

make gate is the OS-claim gate: test-host, both GUEST_OS=none boots, and gate-guest-io (test-guest-net, test-guest-blk, test-guest-console).

• docs/ROADMAP.md: 0.3 trust baseline, 0.4 Debian, guest graphics and x86 VMM, 0.5 persistent x86 desktop, 0.6 Omarchy, 1.0 dual-architecture qualification, and the trust-baseline corrective actions.
• docs/RELEASES.md: evidence-bound release protocol (make release, release-prepare, release-check, release-publish, release-verify).
• CHANGELOG.md: release notes; current line is v0.3.x.
• PLAN.md: active implementation sequencing.
• docs/security-architecture.md: detailed architecture diagrams, capability boundaries, and current security limits.
• Systems and security presentation: editable narrative and claim ledger; native Google Slides publication is pending.

FreeBSD 15.0 AArch64 boots as a guest with the same emulated virtio devices and the same VMM as Linux. make demo-test is the acceptance gate for concurrent authenticated SSH beside Linux; that qualification remains open. Use docs/demo.md for current commands. docs/freebsd-vm-guest.md is historical.

• Language policy: first-party code is C, Rust, or Assembly — target code, host tools, tests, generators, and skill helpers alike. No Python, JavaScript, Go, Zig, or HTML/CSS anywhere in the repository, including vendored code. make policy-check enforces this.
• No human UI in this repository. agentctl (CLI) is the only in-tree consumer; GUIs live in external repositories.
• Contracts before callers: IPC contracts under kernel/agentos-root-task/include/contracts/, queue layouts under platform/include/platform/.
• Do not extend museum PDs (docs/TCB.md). Do not pass QEMU devices through to guests. Do not add guest drivers for a class that has a virtualizer.
• Run make test-host before pushing; OS-level claims need make gate.
• Tasks are tracked with mac task (project agentos), not GitHub issues or TODO lists. See AGENTS.md.
• Developer guide: docs/DEVELOPER_GUIDE.md.

Part 13 of an ongoing chronicle. ← Part 12: Theseus | Part 14: Artlab → Chronicle index · Ordered by first recorded AI-assisted commit.

The programmer had decided that an operating system for agents should begin with a question of ownership.

“Who owns the device?” he asked.

Sir Reginald von Fluffington III was lying across the keyboard. The answer seemed settled.

The programmer meant the device frame, the interrupt, and the authority to use them. He wanted one owner per device class, separate components to share access, and guests that saw a defined interface rather than whatever happened to be underneath. Sir Reginald already operated a capability system in which everyone possessed the ability to request the chair and only he possessed the ability to occupy it.

seL4 supplied the microkernel. The root task distributed memory and capabilities, started the protection domains, and then parked. The programmer considered this a model of responsible management: establish clear authority and cease interfering. Sir Reginald had practiced the second half for years.

Drivers would own devices. Virtualizers would multiplex them. Virtual-machine monitors would present virtio devices to Linux and FreeBSD guests. Native agents would use the shared contracts too, without becoming trusted merely because they described themselves as helpful.

“That part matters,” the programmer told the cat. “Being an agent does not make you part of the trusted computing base.”

Sir Reginald opened one eye. Being a cat apparently did.

The README acquired a table separating what booted today from the intended architecture. A console virtualizer still embedded as a library was described as such. QEMU was the prototype hardware, not proof that every real board already worked. The programmer resisted the temptation to let the diagram outrun the machine, which required more restraint than drawing the diagram.

There would be no human user interface inside the platform. Human-facing applications could live elsewhere and speak its contracts. Sir Reginald approved of this separation in principle by moving to another chair, though the official record continued to show no endorsement.

“Elegant,” the programmer concluded.

Sir Reginald withheld access to the keyboard pending a satisfactory explanation of the food-bowl interrupt policy.

BSD 2-Clause. See LICENSE. libvmm/ carries its own licenses (see libvmm/LICENSES/).

Built on seL4 and libvmm from the Trustworthy Systems group, UNSW.