A capability kernel for on-device AI.

Every dynamic thing is a capability.

A task, a memory mapping, a device, an interrupt route: each exists as a capability, a self-authenticating grant over a fixed set of physical resources. There is no table of issued capabilities, no root user, and no ambient authority behind them to escalate into.

A capability record carries its own proof: a 128-bit AES-CMAC stamp over its identity, rights, kind, epoch, holder and the chain of ancestors it was derived from. Only the kernel holds the stamping keys, which are seeded from hardware entropy and derived per epoch. A program can read a record's fields; it can't mint one or check one.

Records live in a per-task capability arena, mapped read-only into the task so it can read its own holdings without a call. The kernel still trusts none of it: it re-verifies a record's stamp each time a session uses it, so a corrupted slot fails, and a record presented by any task other than its holder is inert. Disclosing a capability never transfers it.

A system call is a transaction.

Kore's whole kernel vocabulary is three verbs: derive, revoke and rendezvous. Mapping memory, spawning a task, killing one and sending a capability are each one of the three, applied to a resource of the right kind.

A program batches up to 107 operations into a session and crosses into the kernel once. The kernel validates the batch, prepares it without side effects, then commits it all or nothing, with a single revocation pass for the whole batch. A later operation can bind the result of an earlier one, so building a process — its address space, pages and capabilities — is one crossing, and starting it is a second.

Commits are optimistic and lock-free. Only revocation conflicts: sessions whose capability footprints don't overlap commit in parallel on different cores, and there is no global kernel lock to serialize them.

Data takes a separate path. Bulk I/O runs on submission and completion rings byte-compatible with Linux io_uring, so code written against liburing ports by swapping headers. The rings live in memory shared between user-space peers rather than in the kernel, and a completion names a slot and a status, never a capability, so no authority can move asynchronously.

Specified before it was built.

Kore implements KRAPH, a formal model of a capability kernel in which every change of authority is a mutation of one finite set of capabilities, plus append-only epoch keys. Physical resources, their topology and the rules of derivation are fixed at boot; only the capability set moves.

The model states 28 axioms and proves 19 theorems from them, among them provenance rootedness, authority monotonicity, closure of descendant revocation, and serializability of sessions that don't conflict. Each axiom is shown to be independent: drop it, and a theorem that held fails.

The code carries the model in its types instead of restating it. A capability value is the model's record. A derivation rule is a trait bound, so an unlawful derive doesn't compile. Identities are fresh and never reused, the premise of the uniqueness theorem.

The proofs are written by hand, and the model is written to be mechanized: first-order over finite sets, with TLA+, Isabelle/HOL and Coq as targets. Mechanized proofs are not part of Kore yet, so we call it formally specified, not formally verified.

Processes and threads fall out of derivation.

The kernel knows only tasks. A task is its capability cross-section: an address space, and the capabilities derived under it.

A thread is a task that shares its parent's address space; a process gets a fresh one. Revoking a thread's root stops that thread, revoking an address space ends the process, and one level up ends a job, each with a single revoke. Device DMA bindings derive under the same address space, so ending a process tears down its DMA in the same cascade.

A new task starts from a role-tagged handle table in its own image: no environment strings, and no name server to look things up in. It reaches exactly the services its founder granted it. At boot, every service image is checked against the BLAKE3 digest in the boot manifest before it runs.

A fatal fault or a panic in a user process ends that process and hands its parent a bounded crash report. It never unwinds through kernel code.

Physical addresses never leave the kernel.

Kore runs its drivers in user space, so its device contract exists to make a faulty or hostile driver harmless to everything it wasn't handed.

Every DMA goes through the IOMMU: Intel VT-d, AMD-Vi or Arm SMMU. A device's translation starts closed — until its driver binds it, its DMA is blocked — and there is no identity-mapped or host-memory fallback. Devices see I/O virtual addresses and programs see capabilities; neither ever sees a physical address.

The kernel enumerates PCIe and holds every device as a capability. A driver claims one through a device broker by vendor, device or class, then derives exactly the registers, interrupt routes and DMA windows it declared. Interrupts arrive as remapped MSI on a route the driver holds and parks on; the kernel wakes it and is otherwise off the path.

Memory is shared by lease: one physical extent mapped into several address spaces, with no copies and a single owner. Revoking the lease unmaps it everywhere and frees it exactly once. Shared libraries are leases too, so a vulnerable library can be retired from a running system: its users fault cleanly instead of reading freed memory.

One policy layer, bounded by capabilities.

Kore separates resource mechanism from resource policy. Run queues, timers, page tables and interrupt routes carry decisions but don't make them. One policy layer in the kernel, the manifold, does: which core runs a waking task, which memory pool backs an allocation, when a task moves, how long a time slice lasts, how deeply an idle core sleeps, how CPU performance is requested, and which CPU takes a device interrupt.

It weighs all of them against one shared model of the machine, instead of a separate heuristic per subsystem. The model is built from firmware topology (ACPI SRAT, SLIT and HMAT, or the device tree), per-core capacity measured at boot, live hardware feedback where the processor provides it (Intel's HFI today) and observed demand. CPU and memory are judged together, so a node short on either is avoided, and performance, efficient and low-power cores are told apart by measured capacity rather than by vendor-specific rules.

Capabilities bound every choice: KRAPH decides which bindings are lawful, and the manifold picks among them. A task is placed only on cores it holds a CPU share for, a migration re-checks that authority at its destination, and no hint can widen the set.

Programs state requirements, not placements. An allocation names its size, alignment, DMA reach, cache attributes and an optional NUMA hint; a service may prefer a core class, which is weighed but never a pin. Each task can read a kernel-written execution-advice word — its CPU, core class, vector width and cache sizes — without a system call.

The manifold governs host CPUs and memory. GPU and NPU queues and device memory belong to their drivers and to Cosmos's user-space compute scheduler.

GPU and NPU drivers with nothing in between.

Kore's Intel Xe GPU and NPU drivers are native user-space providers. A capability-backed process owns the device and its mappings directly: no kernel-mode and user-mode driver split, and no ioctl compatibility layer.

Silicon generations are types, selected once. Lunar Lake's Xe2 GPU and NPU 4 are validated; Panther Lake's Xe3 GPU and NPU 5 are supported. The NPU driver parses, relocates and seals compiled model images itself, cross-checked byte for byte against Intel's reference loader. Device firmware is pinned and verified by BLAKE3 digest.

This is the path Cosmos's local inference takes. On the Lenovo Yoga 7 2-in-1, Qwen3.6-35B-A3B is larger than the machine's memory, so its routed experts stream from NVMe into GPU-visible memory through Kore's storage engine, which reads the drive at its own ceiling.

Guests are ordinary tasks.

What can run as a guest shouldn't have to be ported. Kore's hypervisor has two halves: a world switch in the kernel, where each virtual CPU is an ordinary scheduled task, and the virtual machine monitor, a user-space service.

A guest's memory is one guest-physical map, projected at once into the CPU's second-stage tables (Intel EPT, AMD NPT) and the IOMMU's, so the guest's CPUs and its devices see the same memory under the same rules, with strict W^X at the second stage.

Intel VMX and AMD SVM are implemented. Today's guests are small — C programs, MicroPython and multi-CPU test guests over virtio — and restart cleanly on Intel and AMD hardware. Larger guests are the work in progress.