AetherOS
Private R&D | v0.1

Project hub

The operating system for the sovereign machine.

AetherOS is a capability-first personal computer built from first principles: privacy by construction, universal execution through AetherIR, a formally minded Liminal microkernel, and generative continuity co-piloted by a local twin - never telemetry-first, never ambient authority.

Phase Bootstrap+
Demo gates D1-D5 green
Updated 2026-07-29 | authority flow + L0 model + layer chassis
License Proprietary

This page is the living map of inception, architecture, and what is proven under QEMU - not an install CD and not a public source dump.

Where we are

Honest status as of the last kernel + host wave. Green means observed under test or QEMU serial, not marketing.

D1

Kernel isolation

UEFI boot, caps, ring-3, private VSpace CR3, timer, preemptive RR, IRQ steal.

D2

Runtime fabric

Hand JIT + CLIF interpret + CLIF→native x86 emit (triple parity on demos).

D4

Swarm crypto

Triangle AEAD + multi-hop + WAN TCP multi-hop lab with cover on the wire.

What it can do now

Shipped slices you can exercise on the lab host today.

Liminal microkernel (QEMU/UEFI)

  • Freestanding Rust no_std boot via bootloader 0.11 + OVMF
  • Capability table + SerialWrite isolation demo (A ok, B denied)
  • Per-task VSpace, ring-3 enter, int 0x80 syscalls
  • Yield-RR across dual VSpaces + timer IRQ frame steal
  • Virtio modern: rng, multiport console CTRL+TX, blk R/W + MULTI+FLUSH
  • Legacy virtio fallbacks when modern path unavailable

Host fabric crates

  • AetherIR → hand JIT + CLIF interpret + CLIF native emit
  • VeilNet grants + multi-hop path grants + cover scheduler
  • WAN TCP multi-hop AEAD lab + multi-process cover daemon (OPEN/TICK/REVOKE)
  • Timeline engine + twin shell surface
  • Verification ladder + Verus-shaped invariant document
  • Stub compositor / minifb GUI shell

QEMU serial markers (subset)

Liminal freestanding boot OK
ring3+VSpace isolation OK
virtio-rng modern entropy OK
virtio-console multiport CTRL+TX OK
virtio-blk modern WRITE+READ OK
virtio-blk modern MULTI+FLUSH OK
ring3 IRQ steal OK
boot OK

Full architectural plan

Seven layers. Layer 0 is the root of authority; upper layers never invent ambient rights. Expand a layer for depth. Scan the authority flow first.

Live / lab green Design / stub / scaffold Deferred

Cross-layer authority flow

Human is root of trust. L0 holds pure capability authority. L3 may only birth packets under EgressGrant. L6 twin and timeline paths do not invent ambient egress; they reuse grant hygiene. L1/L4/L5 never mint network rights on their own.

Authority edges (never ambient)
Human root of trust
  -> L0 Liminal microkernel (Live under QEMU)
       -> L1 agents (Design + stubs): only via held caps
       -> L2 runtime fabric (IR + JIT host): capability host rights only
       -> L3 VeilNet (Phase0 + multi-hop lab): EgressGrant packet birth only
       -> L6 swarm + timeline (host paths): twin egress only under explicit grant
L4 compositor (stub) presents; does not invent rights
L5 hardware synthesis (deferred): no rights invented yet
L6 --grant hygiene--> L3
L3 --no grant--> quiet (no packet)

L0 capability object model

Liminal does not grant ambient network or file rights at birth. Authority is carried in capability objects. Design lineage includes seL4-style caps, remixed into Liminal's own model - not an seL4 Isabelle import.

CSpace / caps

Capability table entries. Rights are explicit slots, not ambient process privileges. SerialWrite isolation demo: A ok, B denied.

Frame

Physical memory rights mapped into a VSpace. No ambient mapping of foreign frames without a held cap.

VSpace

Per-task address space with private CR3. Ring-3 enter via iretq; isolation proven under QEMU serial.

Endpoint

Explicit IPC path. Messaging is capability-gated, not ambient sockets.

SchedContext

Scheduling authority for preemptive RR and timer IRQ frame steal across dual VSpaces (lab green).

No ambient net/file

Construction rule: a fresh domain starts with zero network and zero ambient file authority. Upper layers may not invent those rights.

L0 objects and isolation path (public model)
CSpace/caps -> Frame
CSpace/caps -> VSpace -> Ring-3 tasks
CSpace/caps -> Endpoint -> Explicit IPC
CSpace/caps -> SchedContext -> Preempt RR / IRQ steal
No ambient net or file rights -.-> CSpace
QEMU: boot -> ring3+VSpace OK -> dual VSpace RR -> IRQ steal OK

Layer map (progressive disclosure)

Collapsed row: id, title, status. Expand for purpose, evidence, non-goals. Status tags stay calibrated.

L0 Liminal Microkernel Live under QEMU

Pure capability authority (seL4 lineage), frames/VSpaces, endpoints, SchedContext. No ambient network or file rights.

Evidence: freestanding boot, cap table isolation, private VSpace CR3, ring-3, Yield-RR, IRQ steal, virtio rng/console/blk under QEMU. Object model above. Related gate: D1.

L0 object model

L1 Aether Agent Swarm Design + early host stubs

Sandboxed local AI operators: binary archaeologist, API cartographer, security guardian, cognitive companion, UI weaver, driver synthesizer.

Non-goal today: shipping autonomous product agents. Agents act only through held L0 caps; no ambient network from any agent role.

L2 Universal Runtime Fabric IR + JIT live on host

Load ELF/PE/Mach-O, lift to AetherIR, NBTE AOT/JIT cache, OS personalities - foreign binaries enter a capability host, not Wine-as-architecture.

Proven on host: hand JIT + CLIF interpret + CLIF native emit (D2). Full multi-personality and HostSys depth remain mid cliffs. Related: N1 cranelift-jit feature.

L3 VeilNet Privacy Fabric Phase0 + multi-hop swarm

EgressGrant objects only. Personal mix ring, cover morph, grant-bound cells. Construction property: no external packet without a live grant.

Host fabric lab green (D3/D4). Kernel NIC / full mix deferred. Upper layers request grants; they do not invent ambient egress.

Grant lifecycle

L4 Generative Spatial Compositor Stub compositor

Living UI weaver and spatial compositor; multi-modal input (touch, voice, gesture; BCI deferred).

Stub / minifb shell only. Presentation surface does not mint network or file rights. BCI remains deferred.

L5 Hardware Synthesis Deferred

On-demand driver synthesis under formal constraints; device fingerprint; verified Linux driver shim path (later).

No rights invented while deferred. When active, drivers must still enter through capability constraints.

L6 Personal Swarm & Temporal Continuity Mesh + timeline host paths

Owned-device mesh, encrypted digital twin, timeline fork engine for experiment and rollback. Hardware is disposable; the man is root of trust.

Host timeline fork/discard/merge green (D5). Twin egress only under explicit grant (P7). Cross-device durability is a mid cliff, not claimed finished.

Fork hygiene

Grant continuity

How packets are born, how cover dies with grants, and how timeline forks keep experimental egress from leaking into the parent world.

Host fabric lab (D3-D5 green under lab / QEMU paths) Kernel NIC caps, full mix, COW kernel timelines: design or deferred

VeilNet is not a default-deny firewall bolted on later. It is a construction property: a fresh domain has zero network authority. External packets exist only while a live grant says they may. Cover traffic is charged to that grant and ceases when the grant dies. Timeline forks carry experimental grant worlds; discard revokes them; merge never auto-imports net grants without an explicit human gate.

Objects

EgressGrant

Capability object that authorizes packet birth for a subject domain. Scope, rights, budget, and cover binding are part of the object, not ambient policy files.

Path grant

Multi-hop authorization along an owned-device or lab path. Intermediate hops do not invent ambient clearnet rights. Observed on host multi-hop WAN TCP lab paths.

Cover cell

Grant-bound cover schedule. While the grant is live, cover may run; when the grant is revoked or expires, cover stops. Idle domains stay quiet by construction.

Experimental grant world

A timeline fork's tagged grant set used for experiment. Discard tears the world down. Merge into parent requires hygiene so residual egress cannot sneak through.

Three VeilNet laws

  1. Packet birth. External TX requires a live EgressGrant (or composed path grant). No grant means no packet.
  2. Cover bound to grant. Live grant implies cover charged to that grant's lifetime. Cover is not a free ambient presence channel.
  3. Trust is explicit. Peers are untrusted by default. Crypto and predicates, not ambient trust domains, authorize exchange.

Grant lifecycle

Lab control plane words OPEN / TICK / REVOKE describe a multi-process cover daemon exercise on the host fabric. They are not a public consumer API and not a claim of production mesh deployment.

EgressGrant lifecycle (public model)
NoGrant --mint--> GrantLive --packet birth / cover--> GrantLive
GrantLive --REVOKE or expiry--> Revoked --> Quiet (idle = quiet)
NoGrant: no ambient egress path exists

Timeline fork hygiene

Demo gate D5 is green on host timeline engine paths: fork, discard, and merge of experimental continuity. This is not a claim of full kernel COW snapshots or cross-device timeline migration. Those remain later phases.

Fork, discard, merge with grant hygiene
Main --fork--> Exp --mint scoped grants--> LabWorld
LabWorld --discard--> Sink (grants dead, no residual egress)
LabWorld --merge + HumanGate--> Main (no auto net grants)
Twin egress only under explicit grant

Principle map

Principle Object / mechanism Demo gate
P1 Privacy is ontological EgressGrant packet birth; cover bound to lifetime; idle quiet D3
P6 Temporal sovereignty Fork experimental grant worlds; discard revokes; merge with hygiene D5
P7 Cognitive sovereignty Encrypted twin leaves the swarm only under an explicit grant D5 / L6

What it aspires to be

Manifesto constraints - the north star that keeps every cliff honest.

  1. Privacy is ontological - no ambient network path exists to forget to close.
  2. Universal execution - foreign binaries compile into a capability host via AetherIR.
  3. Formal foundations - security climbs a verification ladder; it is not asserted in marketing.
  4. Generative continuity - the UI is alive and local; the twin never phones home by default.
  5. Hardware is disposable - devices are projection surfaces for a personal swarm.
  6. Temporal sovereignty - fork timelines to experiment; discard or merge with grant hygiene.
  7. Cognitive sovereignty - the encrypted twin leaves the swarm only under an explicit grant.

What is coming

True remaining cliffs after the modern MULTI+FLUSH / CLIF / multi-hop / Verus-hooks wave. Near is ship order. Mid is real architecture surface still under-sold by a flat four-item list. Never is deferred by design.

Proof surface: QEMU serial Proof surface: host lab Scaffold / design Deferred / never without ask

Near (ship order)

N1

cranelift-jit feature

cranelift-jit Cargo feature gated; emitter API ready - wire real Cranelift crate next.

host lab / empty feature P2 universal execution

N2

Multi-host WAN standing service

Two-daemon TCP control lab is green; next is process-per-host durable standing service. Not claimed done.

host lab green today P1 privacy | P5 swarm

N3

Verus toolchain port

Invariants documented; hooks scaffold. Next is real proof fn discharge on a Verus toolchain.

scaffold (T3) P3 formal foundations

N4

Virtio-net + port1 data

Multiport control path proven; extend to virtio-net and non-console serial port data queues. No virtio-net green claimed today.

QEMU cliff P1 no ambient NIC

Mid (architecture gaps, not polish)

These are real remaining surfaces already admitted by layer tags and lab boundaries. They are not secret green work and not claimed finished.

M1

Kernel-integrated VeilNet TX

Host Phase0 + multi-hop labs are green. Grant-bound egress inside the guest kernel / NIC path is not claimed.

design boundary P1 ontological privacy

M2

Kani runnable CI (T2)

Kani-shaped harness intent exists as scaffold. Runnable green Kani CI is not claimed.

scaffold P3 formal ladder

M3

L1 agent swarm crates

Design + early host stubs only. Not a shipping local AI operator product.

design + stubs P4 | P7

M4

L4 compositor beyond stub

minifb / stub compositor only. Living UI weaver is not a shipped product surface.

stub P4 generative continuity

M5

Personality / FS grant-only depth

IR + JIT live on host. Full multi-personality and HostSys FS grant demos remain deeper cliffs.

partial host P2 universal execution

M6

Cross-device timeline durability

Host fork / discard / merge paths are green. Cross-device timeline migrate is later phase, not claimed.

host paths only P5 | P6 | P7

Explicitly deferred / never without ask

…

Hard non-goals

Full Cocoa/Win32 as core UI | seL4-complete Isabelle | neuromorphic / BCI | bare metal without an explicit ask.

deferred by design

Verification ladder

AetherOS does not claim seL4-complete proofs. The ladder is tracked in public language here so expectations stay calibrated. Security climbs; it is not asserted in marketing.

Demo gates D1-D5 green means lab observation under QEMU serial and host tests. That is not the same as model-checked or proof-discharged security. Tier 0-1 are the live floor today. Higher tiers are scaffold, planned, or design-compatible only.

Status vocabulary

Active

Runs in the lab now: rustc, cargo test, and authored cap property tests.

Scaffold

Shapes, hooks, or design docs exist. Not a green proof CI suite and not discharged proof functions.

Planned

Direction of climb only. Full Verus / Lean proofs are not claimed.

Design-compatible only

Lineage may be compatible with an seL4-style substrate. Not an Isabelle-complete import and not a forked verified kernel.

Ladder climb

Verification tiers (honest stop-lines)
T0 rustc + cargo test ACTIVE
T1 Cap property tests ACTIVE
T2 Kani SCAFFOLD
T3 Verus-style hooks SCAFFOLD
T4 Verus / Lean full proofs PLANNED (not claimed)
T5 seL4 substrate option DESIGN-COMPATIBLE ONLY
D1-D5 lab evidence feeds T0-T1 only

Demo gates to evidence class

Each green gate has a primary evidence class. Empty formal cells are intentional: gates do not invent Tier 4 proofs.

Gate Lab claim Evidence class Ladder touch
D1 Kernel isolation under QEMU Runtime observation (serial markers) T0 (+ tests where present)
D2 Hand JIT + CLIF interpret + native emit Host behavioral demo + unit tests T0
D3 Deny-by-default packet birth; cover bound Host lab / property intent T0-T1
D4 Triangle AEAD + multi-hop WAN TCP lab Host lab demo (not crypto formal proof) T0
D5 Fork / discard / merge host paths Host behavioral demo T0

Tier scan table

Tier Tool Status
0rustc + cargo testActive
1Cap property testsActive
2Kani model checkingScaffold
3Verus-style hooksScaffold
4Verus / Lean full proofsPlanned
5seL4 substrate optionDesign-compatible only

What each tier buys

T0 rustc + cargo test Active

Buys: typecheck and unit tests on paths that run in lab.

Does not buy: kernel isolation theorems or machine-checked refines-to-binary proofs.

T1 Cap property tests Active

Buys: authored property / invariant tests where present.

Does not buy: model-checked or proof-discharged caps.

T2 Kani model checking Scaffold

Buys: harness intent and cfg-shaped hooks.

Does not buy: a claimed green Kani CI suite.

T3 Verus-style hooks Scaffold

Buys: Verus-shaped hooks and a design invariant document.

Does not buy: real proof fn discharge on a Verus toolchain.

T4 Verus / Lean full proofs Planned

Buys: direction of climb only.

Does not buy: any complete kernel proof today.

T5 seL4 substrate option Design-compatible only

Buys: capability lineage compatible with seL4-style authority as a design option.

Does not buy: seL4 Isabelle completeness or a verified seL4 fork shipping as AetherOS.

Inception

Why this project exists as its own category.

AetherOS is not a music generator, journal app, wellness tracker, or Linux rice. It is a local-first, privacy-sovereign multi-layer personal computing system - a microkernel plus fabric plus swarm - aimed at people who want authority to be explicit, execution to be hostable, and intelligence to stay on-device.

Design lineage is honest about its teachers: seL4-style capabilities, Zircon-like bulk memory rights, Genode-like recursive worlds, Barrelfish-like explicit messaging later - always remixed into Liminal's own object model rather than a fork.

Private monorepo (offline git + survival mirrors). This site is the shareable surface for architecture and progress - the source remains proprietary R&D.

FAQ

What is AetherOS?

A ground-up capability-first personal OS research project: Liminal microkernel, VeilNet, AetherIR fabric, personal swarm and timeline continuity.

Is it open source?

No. Proprietary private R&D. This hub tracks vision and status; it is not a public source tree.

Is it a Linux distro?

No. Freestanding Rust no_std kernel plus host crates - not a distro or kernel fork.

What is VeilNet?

Deny-by-default network fabric. Packets require a live EgressGrant; cover is grant-bound so idle stays silent.

How is AetherOS layered?

Seven layers: capability microkernel through personal swarm and temporal continuity. Upper layers never invent ambient authority.

Can I run it?

Lab builds target QEMU/UEFI on a development host with Rust + QEMU. There is no public consumer installer yet.

How is an external packet born?

Only under a live EgressGrant (or composed path grant). A domain with no grant has no ambient egress path. See Grant continuity.

What happens to cover when a grant dies?

Cover is bound to grant lifetime. On REVOKE or expiry, cover ceases. Idle domains stay quiet by construction on host fabric lab paths (D3).

What does timeline discard do to grants?

Discard drops the experimental branch and must revoke experimental egress so no residual packet birth remains. Merge does not auto-import net grants without an explicit human gate (D5 host engine paths).

Can the digital twin phone home by default?

No. Cognitive sovereignty: the encrypted twin leaves the personal swarm only under an explicit grant. There is no ambient twin egress channel.

What is actually proven today?

QEMU serial markers and cargo / cap property tests (Tier 0-1 Active). Demo gates D1-D5 are lab-green, not machine-checked full proofs.

Does Scaffold mean almost proven?

No. Scaffold means hooks, shapes, or design docs exist. It is not running proof CI and not discharged Verus or Kani suites.

Is AetherOS seL4-proven?

No. seL4-style capabilities are design lineage. Tier 5 is design-compatible only. Isabelle-complete seL4 is explicitly deferred.

Can outsiders audit formal proofs?

No public source tree. The monorepo is proprietary R&D. This hub publishes calibrated status, not proof artifacts.