Lab bootable
QEMU/UEFI freestanding boot, D1-D5 green, virtio + host fabric labs. Already shipping evidence on this map.
Done under QEMUProject hub
The operating system for the sovereign machine.
AetherOS is a capability-first personal OS research project: privacy by construction (VeilNet grants), universal execution via host AetherIR (hand JIT + CLIF paths), Liminal microkernel isolation under QEMU, and a local twin shell that leaves only under an explicit grant - never telemetry-first, never ambient authority. Formal claims climb a public verification ladder (T0-T1 active).
This page is the living map of inception, architecture, and lab evidence. Green means QEMU serial and/or host lab observation - not an install CD and not a public source dump.
Planning horizon (~18 months)
Ambition bar for a personal-class OS path, not a Continuum gate counter. Lab gates can stack high while product cliffs (real Verus Tier 4, Fabric TX product, compositor, agents, multi-site WAN, kernel AEAD hop peel) still dominate the remaining road. Estimate only; not a ship date.
Now: D1-D327 lab depth
Ambition ~32% | not done
Lab depth (D1-D327); product cliffs remain | lab D1-D327 | ambition 35% of ~18mo
Interactive lab (not product appliance)
Continuum D6-D327 is deep lab green: Bar B, dual-path reverse co-order, product SiteId, onion SURB, two-process named-pipe WAN, and guest-directed AEAD hop peel (D308-D327). Research proof surface only. Not a daily interactive appliance or product net stack. ChaCha is not in the kernel image. Multi-machine WAN is not done.
Lab green | product openArchitecture product cliffs
Most of the remaining road: real Verus Tier 4 (not executable discharge), guest Fabric TX product path, compositor beyond stub, agent swarm crates, multi-site WAN product, kernel-resident AEAD (D328), personality/FS depth. Guest-directed peel D308-D327 is lab green (host ChaCha). Lab sketches do not close the product cliffs.
Mid cliffs | long runwayPersonal-class trajectory
Toward a machine you could live in: durable swarm, stronger formal story, UI/twin continuity. Bare metal and daily-driver polish only with explicit ask. Not a Windows replacement promise.
Ambition bandSupport independent R&D if this map is useful to you. Cash App: $JonBaileyxyz.
Inception
Why this project exists as its own category.
AetherOS 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.
HARDWARE IS DISPOSABLE. YOUR OS SHOULD MOVE WITH YOU ACROSS DEVICES.
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.
Principle enforcement
Manifesto constraints as an index into architecture, lab gates, and cliffs. Not a proof certificate and not marketing.
Constraint index over existing map chapters
| Principle | Layers | Mechanism | Gate / cliff | Map |
|---|---|---|---|---|
| P1 Privacy is ontological | L0 L3 L6 | EgressGrant; cover bound; zero net at birth | D3 D4 / N4 M1 | Grants | Lab | Adversary |
| P2 Universal execution | L2 | AetherIR + triple path into capability host | D2 / N1 M5 | Runtime |
| P3 Formal foundations | cross | Ladder T0-T1 active; T2-T5 calibrated climb | D* -> T0-T1 / N3 M2 | Verify |
| P4 Generative continuity | L4 L1 | Local UI/twin; no ambient phone-home | stub / M3 M4 | Arch L4 |
| P5 Hardware disposable | L5 L6 | Devices as projection; swarm continuity | deferred / N2 M6 | Cliffs |
| P6 Temporal sovereignty | L6 | Fork/discard/merge + grant world hygiene | D5 / M6 | Grants |
| P7 Cognitive sovereignty | L6 L1 | Twin egress only under explicit grant | D5 / M3 M6 | Grants |
Manifesto one-liners
- Privacy is ontological - no ambient network path exists to forget to close.
- Universal execution - foreign binaries compile into a capability host via AetherIR.
- Formal foundations - security climbs a verification ladder; it is not asserted in marketing.
- Generative continuity - the UI is alive and local; the twin never phones home by default.
- Hardware is disposable - devices are projection surfaces for a personal swarm.
- Temporal sovereignty - fork timelines to experiment; discard or merge with grant hygiene.
- Cognitive sovereignty - the encrypted twin leaves the swarm only under an explicit grant.
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
Proven vs plan vocabulary
Collapsed layer lines state what is proven. Expanded depth may describe architectural plan. Green tags never mean full plan complete.
| Do not read as now | Allowed now | Plan / cliff |
|---|---|---|
| Full ELF/PE/Mach-O product loaders | IR + JIT + CLIF host demos (D2) | N1 cranelift-jit; M5 personalities |
| Personal mix ring as finished product | Phase0 grants + multi-hop host lab | Full mix; kernel NIC (M1) |
| Living UI weaver as shipping UI | Stub / minifb compositor | M4 compositor beyond stub |
| Twin co-pilot product | Twin shell surface + grant egress | Cognitive companion depth |
| Formally verified kernel | Verification ladder T0-T1 Active | T2-T5 climb (scaffold / planned) |
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.
Diagram source (ASCII)
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.
Diagram source (ASCII)
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
L2 Runtime Fabric Codex
How a foreign binary is intended to enter AetherOS: lift into AetherIR, then execute only under capability-host rights. This is not Wine-as-architecture and not a claim that every loader format is product-complete.
Host lab green (D2): hand JIT + CLIF interpret + CLIF native emit
Plan / cliffs: multi-format loaders, personalities, HostSys depth; cranelift-jit optional feature wired
Universal execution (P2) means foreign code becomes a guest of the capability host via AetherIR. Proven today on the host fabric: hand JIT + CLIF interpret + CLIF native emit, plus optional real Cranelift JIT behind feature cranelift-jit (quad parity on pure arith demos). Full ELF/PE/Mach-O product loaders and multi-personality HostSys remain calibrated cliffs.
Pipeline objects
Foreign binary surface
Architectural intent: ELF/PE/Mach-O intake. Not every format is a finished product loader on the public map.
AetherIR
Intermediate representation for host execution paths. Lift/decode feeds the IR; rights stay outside the IR itself.
Triple execution path
Hand JIT, CLIF interpret, and CLIF native emit with parity demos under D2 on the host lab.
Capability host
Execution only with held caps. No ambient net or file rights are invented by the runtime fabric.
Diagram source (ASCII)
Foreign binary (plan: ELF/PE/Mach-O) -> Lift / decode -> AetherIR -> Hand JIT (D2 green) -> CLIF interpret (D2 green) -> CLIF native emit (D2 green) -> Capability host rights only (no ambient net/file) -.-> Personalities / HostSys (M5 mid cliff) -.-> cranelift-jit feature (N1 lab green, optional deps) Not Wine-as-architecture. Host lab != guest kernel universal exec claim.
Proven vs design
| Item | Status | Proof surface | Note |
|---|---|---|---|
| Hand JIT | Active (host) | D2 host demos / tests | Part of triple parity |
| CLIF interpret | Active (host) | D2 host demos / tests | Oracle / parity path |
| CLIF native emit | Active (host) | D2 host demos / tests | native_loop demos |
| Full multi-format loaders | Design / partial | Architectural intent | Not product-complete on map |
| Personalities / HostSys depth | Mid cliff M5 | Host design surface | Grant-only HostSys demos later |
| cranelift-jit crate | Lab green (feature) | Optional feature on | Real Cranelift JIT; default build stays light |
Principle map
| Principle | Mechanism | Gate / cliff |
|---|---|---|
| P2 Universal execution | AetherIR + triple path into capability host | D2 / N1 / M5 |
| P1 Privacy ontological | Hosted code gets no ambient net; egress still needs grants | D3 + L3 |
| P3 Formal foundations | D2 is host behavioral + tests (T0), not translation proofs | #verify |
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.
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
Proven on host (D2): hand JIT + CLIF interpret + CLIF native emit (triple parity demos). Foreign binaries are intended to enter a capability host, not Wine-as-architecture.
Plan (not all green): ELF/PE/Mach-O loaders, NBTE AOT/JIT cache, multi-personality HostSys (M5). N1 real Cranelift is optional feature lab green. IR + JIT host is the live tag.
L3 VeilNet Privacy Fabric Phase0 + multi-hop swarm
Proven on host (D3/D4): EgressGrant packet birth, multi-hop path grants, cover bound to live grants. Construction property: no external packet without a live grant.
Plan (not all green): personal mix ring, cover morph, full mix profiles, kernel NIC TX. Tag remains Phase0 + multi-hop lab. See Grant continuity.
L4 Generative Spatial Compositor Stub compositor
Proven today: stub compositor / minifb shell only. Generative spatial compositor is design language, not a shipping product surface.
Plan (not green): living UI weaver, multi-modal input (touch, voice, gesture). BCI remains deferred. Tag stays Stub compositor.
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.
Where we are
Honest status through Continuum D1-D327 (lab). Green means observed under test or QEMU serial, not marketing. D308-D327 is guest-directed AEAD hop peel: host ChaCha opens each layer, and the kernel refuses consume until the peel count matches. Next lab gate: D328 kernel-resident AEAD. Product cliffs remain (real Verus Tier 4, multi-machine WAN, ChaCha inside the no_std kernel).
Where D328 starts states the boundary. The gate is not green.
Kernel isolation
UEFI boot, caps, ring-3, private VSpace CR3, timer, preemptive RR, IRQ steal.
Runtime fabric
Hand JIT + CLIF interpret + CLIF -> native x86 emit (triple parity on demos).
VeilNet grants
Deny-by-default packet birth, cover bound to live grants, idle = quiet.
Swarm crypto
Triangle AEAD + multi-hop + WAN TCP multi-hop lab with cover on the wire.
Timeline
Fork / discard / merge continuity for experimental grant worlds.
Shell residency
Init shell path after lab demos: shell ready + scripted session OK under QEMU. Not a full tty product.
Mini FS
Toy AETHERFS on virtio-blk: superblock LBA 10, file LBA 11, mount/write/read OK. Not ext4/Linux VFS.
Userspace ELF load
Freestanding ELF64 ET_EXEC load: map PT_LOAD, enter e_entry, elf load OK + elf exit observed. Not multi-personality HostSys.
Net application path
Virtio-net app path under QEMU SLIRP: DHCP Offer classification and/or ICMP echo. Not guest Fabric TX or a production stack.
Grant-bound TX sketch
Guest path honesty: deny without grant, allow with OPEN grant, deny after REVOKE. Sketch only - not full Fabric TX on the wire.
Verus lemma A1 discharge
Executable exhaustive discharge of attenuation never elevates. Not a real Verus toolchain Tier-4 proof.
Multiport port1 data
Virtio-console multiport port1 data queue TX under QEMU. Not a full multi-port product.
Timeline cross-device
Host dual-device tip export/import with grant hygiene (grants do not auto-live on import). Not multi-host product mesh.
Grant-bound cover
Cover cells only while a live grant exists; revoke returns to quiet. Not a Loopix product stack.
Runtime bitwise broaden
And/Or/Xor on AetherIR with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff, not a product loader.
WAN multi-reconnect durability
Standing cover host: grant survives 3+ client reconnects, cover while live, REVOKE returns to quiet. Localhost lab only, not production multi-host WAN.
Runtime shift broaden
Shl/Shr on AetherIR with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff; arithmetic right shift.
Runtime CmpNe
CmpNe on AetherIR with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff.
Runtime Not
Bitwise Not on AetherIR with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff.
Fabric-net path honesty
Grant-bound fabric birth plus lab net evidence under QEMU. Not product guest Fabric TX or VeilNet on the wire.
Runtime CmpLt
Signed less-than on AetherIR with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff.
Runtime CmpLe
Signed less-or-equal on AetherIR with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff.
Runtime CmpGt
Signed greater-than on AetherIR with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff.
Runtime CmpGe
Signed greater-or-equal completes the signed icmp set (Eq/Ne/Lt/Le/Gt/Ge) with triple parity. Host runtime cliff.
Runtime Div
Signed integer divide on AetherIR (truncate toward zero) with hand JIT + CLIF interpret + CLIF native triple parity. Host runtime cliff; lab demos avoid div-by-zero and MIN/-1.
Runtime Rem
Signed remainder on AetherIR (after truncate-toward-zero divide) with hand JIT + CLIF interpret + CLIF native triple parity. Completes the Div/Rem pair. Host runtime cliff.
Verus lemma A2
Executable discharge: copy-attenuate rejects elevation (mask must stay subset of src rights). Exhaustive low-byte domain + CapTable corners under QEMU. Not a real Verus Tier-4 proof.
Product loader
Host product load path: multi PT_LOAD ELF64 (ET_EXEC x86_64, entry-in-mapped-range, R/W/X flags) plus fixture IR run under stdout-only caps. Not x86 instruction lift or multi-personality HostSys.
Verus lemma A3
Executable discharge: SerialWrite invoke requires INVOKE and WRITE. Empty slot and wrong type yield InvalidCap; missing rights yield MissingRights. Not a real Verus Tier-4 proof.
ELF instruction lift
Narrow linear x86-64 decode sketch (mov imm / add / ret) from ELF PT_LOAD into AetherIR with hand JIT + CLIF interpret + CLIF native triple parity (result 10). Not a full disassembler or multi-block control flow.
Verus lemma A4
Executable discharge: dual-task CSpace isolation. Task A with SerialWrite may invoke; Task B empty yields InvalidCap; delete A does not revoke B; same slot index is not a forge path. Not a real Verus Tier-4 proof.
ELF lift broaden
Linear x86-64 lift adds imul, and, or, xor, and mov rax,rcx with hand JIT + CLIF interpret + CLIF native triple parity (imul demo result 42). Still linear only; not jcc or multi-block control flow.
Verus lemma A5
Executable discharge: VeilNet packet birth requires open cap, live grant, send right, in-scope dest, and budget. Cover emits only while a grant is live; revoke returns idle quiet. Host fabric lab; not a real Verus Tier-4 proof.
ELF lift jcc
First multi-block control-flow lift: test/jnz diamond with then/else ret arms (cond nonzero yields 42, zero yields 7) with hand multi-block JIT + CLIF interpret + CLIF native triple parity. Sketch only; not general CFG recovery.
Runtime Udiv/Urem
Unsigned integer divide and remainder on the host runtime fabric: hand JIT (xor rdx; div rcx), CLIF interpret, and CLIF native triple parity (udiv demo 12, urem demo 15). Div-by-zero traps. Host lab only; not guest kernel div.
ELF lift loop
First counted-loop control-flow lift: mov/add/dec + backward jnz (triangular sum N*(N+1)/2; n=5 yields 15, n=7 yields 28) with multi-block hand JIT + CLIF interpret + CLIF native triple parity and ELF packaging. Sketch only; not general loop nests or irreducible CFG.
WAN prod durability
Production-shaped dual standing cover hosts beyond D16: five reconnects each with LIVE grant, cover counter continuity, abrupt TCP drop without QUIT still LIVE, selective REVOKE (A quiet while B remains live). Localhost lab only; not routable multi-site product.
CLIF Ushr/Neg
CLIF/runtime broaden: logical shift right (ushr) and two's complement negate with hand JIT + CLIF interpret + CLIF native triple parity (ushr demo 31, neg demo 20). Complements arithmetic Shr and bitwise Not. Host lab only.
ELF multi-jcc
First multi-jcc cascade lift: if/else-if/else with two forward jz branches (c1 nonzero -> 42, else c2 nonzero -> 7, else 3) into a 5-block AetherIR CFG with hand multi-block JIT + CLIF interpret + CLIF native triple parity and ELF packaging. Sketch only; not arbitrary multi-jcc graphs.
Verus lemma A6
Executable discharge: timeline grant hygiene. Fork may record experimental grant ids; discard returns them (cannot discard main); merge and cross-device import copy state only and never auto-activate foreign grants; tampered tip hash rejects. Host lab; not a real Verus Tier-4 proof.
Runtime Select/Cmov
Branchless select on the host runtime fabric: dest = cond != 0 ? a : b via cmovz, with hand JIT + CLIF interpret + CLIF native triple parity (demo result 22). Complements multi-block Branch. Host lab only.
ELF gated loop
First jcc+loop combined CFG lift: forward jz skip-gate around a triangular counted loop body (flag nonzero -> N*(N+1)/2, zero -> 0; demos 15/0/28) as a 5-block AetherIR module with multi-block triple parity and ELF packaging. Sketch only; not general nested loops.
Verus lemma A7
Executable discharge: path-grant multi-hop invents no ambient clearnet. mint_path_grant scopes SwarmPeer(path) only; SwarmPeer never implies ClearnetProfile; off-path and unenrolled hops deny; clearnet-only grants cannot drive multi-hop edges. Host lab; not a real Verus Tier-4 proof.
Runtime unsigned icmp
Unsigned compare set on the host runtime fabric: CmpUlt/Ule/Ugt/Uge via setb/setbe/seta/setae with hand JIT + CLIF interpret + CLIF native triple parity (demo sum 4, including high-bit -1 > 1u). Complements signed icmp. Host lab only.
ELF nested loop
First double-nested counted loop lift: outer M x inner N product of trips (add rax,1 each inner; demos 3x4=12, 5x5=25, 2x7=14) as a 5-block AetherIR module with two back-edges, multi-block triple parity, and ELF packaging. Sketch only; not irreducible or multi-exit CFG.
Verus lemma A8
Executable discharge: cover cells charge grant budget exhaustively. Each cover_tick emission costs one cell + CELL_SIZE bytes (same as payload); exhausted grants stop covering and fail further try_send; cover shares the payload pool; revoke still silences cover. Host lab; not a real Verus Tier-4 proof.
Cranelift multi-block
Real Cranelift JIT multi-block polish (feature cranelift-jit): counted loop, branchless select, double-nested product loop, and diamond branch all pass hand multi-block JIT + CLIF interpret + CLIF native + real Cranelift quad parity (demos 40/22/12/42). Host lab only; optional feature keeps default builds light.
ELF multi-exit loop
Richer CFG lift: multi-exit counted loop with early break (cmp rcx,K; jz early) plus normal back-edge exit. Demos: N=5 K=2 -> 3 trips, K=N immediate 0, N=7 K=3 -> 4. 5-block AetherIR with early and normal Halt, triple parity + ELF packaging. Sketch only; not irreducible multi-entry loops.
Cover wire schedule
Loopix-lite discrete wire cover: period(lambda)=max(1,round(1/lambda)); cover_wire_tick advances a lab clock and emits Loop/Drop when due, charging grant budget (A8). Lab: lambda_loop=1 lambda_drop=0.5 over 10 ticks -> 10 loop + 5 drop cells; ordered wire log; idle after revoke. Host fabric only; not a realtime NIC mixer.
Cranelift ucmp/div
Real Cranelift multi-block ucmp/div polish (feature cranelift-jit): CmpUlt branch to Udiv then-arm (100/u4=25) or signed Div else-arm (20/4=5), plus single-block udiv/div/ucmp breadth (12/8/4) through hand multi-block JIT + CLIF interpret + CLIF native + real Cranelift quad parity. Host lab only.
ELF irreducible loop
Irreducible CFG sketch: two-entry alternating loop (entry A adds 1, entry B adds 2) with external split on a flag so neither entry dominates the other. Demos: N=3 start A -> 4, start B -> 5, N=4 start A -> 6. 4-block AetherIR, triple parity + ELF packaging. Sketch only; not general unstructured relooping.
Payload wire interleave
Successful try_send stamps Payload cells onto the same discrete wire log as Loopix cover (D49). Lab sequence P then Loop (period 2) then P then Loop yields ordered kinds [P, Loop, P, Loop]; denied sends never stamp; payload and cover share grant budget (A8). Host fabric only.
Cranelift multi-exit
Real Cranelift JIT on multi-exit counted loop IR (D48 shape): early break when rcx==K plus normal exit, 5-block CFG, hand multi-block JIT + CLIF interpret + CLIF native + real cranelift-jit quad parity. Demos: N=5 K=2 -> 3, K=N -> 0, N=7 K=3 -> 4. Host lab only (feature cranelift-jit).
Cranelift irreducible
Real Cranelift JIT on irreducible two-entry loop IR (D51 shape): flag splits to entry A (+1) or B (+2) with a cycle so neither entry dominates. 4-block CFG, hand multi-block JIT + CLIF interpret + CLIF native + real cranelift-jit quad parity. Demos: N=3 start A -> 4, start B -> 5, N=4 start A -> 6. Host lab only (feature cranelift-jit).
Wire morph / decoy
Grant-scoped morph profile on EgressGrant. Morph and Decoy cells ride the same discrete wire as Loopix cover (D49) and payload interleave (D52). Rates without a bound profile stay silent; clear morph or revoke idles the streams; cells charge grant budget (A8) and stamp morph_profile on the wire log. Lab: profile=7, lambda_morph=1, lambda_decoy=0.5, 10 ticks -> 10 morph + 5 decoy. Host fabric only (ghost-lan DNA).
Verus A9 wire hygiene
Executable discharge of lemma A9: payload + cover + morph wire interleave hygiene. Denied sends never stamp the wire; morph/decoy require a bound profile; all kinds share one ordered log and one budget pool; revoke idles further emissions. Host fabric only (not real Verus Tier 4).
SURB-like reply
Grant-scoped single-use SURB-like reply tokens. mint_reply_token under a live grant; try_reply stamps CellKind::Reply once, charges budget (A8), and consumes the token. Wrong holder, double-use, unknown token, and dead grant fail closed. Grant revoke burns outstanding tokens. No ambient reply path. Host fabric lab only (not product mix crypto).
Multi-profile morph
Switch morph profiles mid-grant with historical wire honesty. set_grant_morph from A to B to C reseeds the schedule; new Morph cells stamp the active profile; prior stamps are never rewritten. Lab order A-A-A-B-B-B-C-C (3/3/2). Host fabric only.
Verus A10 SURB hygiene
Executable discharge of lemma A10: SURB-like reply token hygiene. No ambient reply; mint requires live grant and subject holder; single-use consume; revoke burns outstanding; successful reply stamps CellKind::Reply and charges budget. Host fabric only (not real Verus Tier 4).
ELF lift + Cranelift e2e
End-to-end host path: static ELF (multi-exit + irreducible two-entry loops) lifted to AetherIR, then hand multi-block JIT + CLIF interpret + CLIF native + real Cranelift JIT quad parity. Demos: multi-exit 3/0/4 and irreducible 4/5/6. Feature cranelift-jit on aether-rt. Host lab only.
Decoy multi-profile
Morph and Decoy co-emit under multi-profile switches on the discrete wire. Each tick stamps Morph then Decoy with the active profile; A/B/C phases preserve historical stamps (A=4 B=4 C=2, decoys=5). Decoy-only streams also switch cleanly. Host fabric only.
Verus A11 multi-profile hygiene
Executable discharge of lemma A11: multi-profile morph stamp hygiene. Profile gate for Morph/Decoy; switch never rewrites history; stamps match active profile at emission. Host fabric only (not real Verus Tier 4).
Payload multi-profile interleave
try_send payload cells interleave with multi-profile morph on the discrete wire. Sequence P then Morph(A) then P then Morph(B) then P under A->B switch; denied sends stay silent; shared budget. Host fabric only.
WAN SURB
SURB-like single-use reply tokens on multi-hop path grants. mint_path_grant (1->2->3) then multi-hop forward (2 edges) then try_reply once; double-use and ambient denied; revoke burns outstanding tokens. Host fabric lab (not product mix crypto).
Triple wire interleave
Full discrete-wire cocktail: payload + morph + decoy under multi-profile switches, then a single-use SURB reply. Order P-M-D-P-M-D-R; Reply carries no morph stamp; historical A stamps survive B phase. Host fabric only.
Verus A12 composite
Executable discharge of lemma A12: composite wire + WAN SURB hygiene. Shared budget unit; Reply never requires morph stamp; composes D63 payload multi-profile, D64 WAN SURB, and D65 triple interleave. Host fabric only (not real Verus Tier 4).
Multi-grant morph isolation
Two live grants emit independent morph streams with distinct profiles. Each Morph stamps its own grant id and profile; budgets stay separate; revoking one grant does not silence the other. Host fabric only.
Verus A13 multi-grant isolation
Executable discharge of lemma A13: multi-grant morph stream isolation. Grant/profile stamp matching; concurrent distinct profiles; revoke A does not silence B; composes D67 lab. Host fabric only (not real Verus Tier 4).
Multi-grant SURB isolation
Reply tokens are grant- and holder-scoped. Cross-mint and cross-consume fail closed; each successful try_reply stamps only its grant; revoking G1 burns only G1 tokens while G2 tokens remain live. Host fabric only.
Verus A14 multi-grant SURB
Executable discharge of lemma A14: multi-grant SURB token isolation. Mint requires subject holder; no cross-domain consume; revoke A does not burn B tokens; composes D69 lab. Host fabric only (not real Verus Tier 4).
Morph+SURB combo
Concurrent multi-grant morph streams and SURB isolation. Two grants emit Morph under distinct profiles while each holds a reply token; cross-reply denied; Morph stamped and Reply unstamped; revoking one grant freezes its morph and SURB while the other continues. Host fabric only.
Verus A15 morph+SURB composite
Executable discharge of lemma A15: multi-grant morph+SURB concurrent isolation. Morph/Reply stamp polarity; composes D67 morph isolation, D69 SURB isolation, and D71 combo labs. Host fabric only (not real Verus Tier 4).
ELF lift Cranelift e2e broaden
Broadens the ELF->lift->real Cranelift path beyond multi-exit/irreducible: nested loop (12), gated loop (15/0), jcc diamond (42), multi-jcc (42), counted triangular (15), with multi-exit regression. Hand JIT + CLIF interpret + CLIF native + real Cranelift quad parity. Feature cranelift-jit on aether-rt. Host lab only.
Linear Cranelift e2e
Linear x86 lift through real Cranelift: add (10), imul (42), and (0x0A) via ELF/raw packaging with hand/CLIF/native/real Cranelift quad parity. Feature cranelift-jit. Host lab only.
Guest grant-tx morph
Kernel GuestFabric morph profile sketch: morph_tick silent without grant or profile; stamps MorphProfileId when bound; clear/revoke quiet. QEMU serial markers + unit discharge. Not product VeilNet morph on wire.
Guest morph budget
morph_tick charges one grant budget cell (same unit as try_birth). Exhausted budget silences morph and denies birth. Shared pool honesty on the guest sketch path.
Guest multi-profile morph
GuestFabric records historical morph profile stamps under A to B to C switches (order A-A-B-B-C). Earlier stamps are never rewritten when the profile changes. Kernel sketch only.
Guest cover budget
cover_tick charges one grant budget cell (same unit as try_birth and morph_tick). Cover, morph, and birth share one pool; exhausted budget silences all three. Kernel GuestFabric sketch; aligns with VeilNet A8.
WAN SURB wire
mesh-crypto multi-hop TCP carries WanCellKind::Reply frames. VeilNet single-use reply tokens stamp discrete Reply and charge budget; no ambient, single-use, revoke burns further mint. Lab wire honesty only; not product mix/SURB crypto.
Multi-grant guest cover
GuestFabric holds two concurrent grant slots. cover_tick_grant charges only the named grant; budgets and cover counts never cross. revoke_grant is scoped; the other grant keeps budget and can still cover. Kernel sketch only; not product multi-tenant fabric.
Multi-grant guest morph
set_morph_grant and morph_tick_grant bind profiles and stamp morph cells per grant only. Two live grants keep independent morph counts and budgets; historical stamps do not rewrite across grants; scoped revoke silences one stream. Kernel sketch; mirrors host D67 isolation DNA.
Multi-grant guest birth
try_birth_grant charges only the named grant. Dual slots keep independent born counts and budgets; scoped revoke denies birth on one grant while the other still births.
Cocktail interleave
Single-grant cover+morph+birth order C-M-B-C-M-B shares one budget pool; exhaustion silences all three.
Dual cocktail isolation
Two grants run independent C/M/B cocktails. Counts never cross; revoke of one leaves the other frozen or live as scoped.
Verus A16 guest cover
Executable discharge of multi-grant guest cover isolation. Not real Verus Tier 4.
Verus A17 guest morph
Executable discharge of multi-grant guest morph isolation. Not real Verus Tier 4.
WAN reverse SURB
Dest opens payload then writes Reply reverse on the same TCP stream. VeilNet single-use + revoke burn. Lab only.
Cover+morph combo
Concurrent dual cover+morph streams with partial revoke; remaining grant keeps emitting.
Verus A18 composite
Executable composite discharge over guest multi-grant cover/morph/birth cocktails. Not real Verus Tier 4.
Guest SURB token
GuestFabric mint_reply_token + try_reply: single-use, no ambient, revoke burns. Charges grant budget. Sketch only; not product SURB crypto.
Multi-grant SURB + morph combo
Tokens never cross-consume across dual grants; concurrent morph streams plus SURB with partial revoke. Kernel sketch.
Multi-hop reverse SURB
Three-node TCP path: intermediate relays Payload forward and Reply reverse. VeilNet single-use hygiene. Lab wire only.
Verus A19-A20
Executable discharge of guest SURB hygiene (A19) and multi-grant guest SURB isolation (A20). Not real Verus Tier 4.
Full cocktails with reply
Single-grant C-M-B-R-C shared budget; dual-grant full C/M/B/R pools isolated.
Verus A21 SURB composite
Executable composite discharge over A18-A20 plus guest SURB cocktails. Not real Verus Tier 4.
SURB + cover budget interleave
Dual-grant reply and cover share each grant budget pool (orders C-R-C-R and R-C-C). Isolation + BudgetEmpty after drain. Sketch only; not product SURB crypto.
WAN co-emit + dual CMR depth
WAN TCP SURB co-emit Morph (P-M-R) and Cover (P-C-R). Guest dual SURB+cover+morph, morph starvation isolation, Verus A22. Lab only.
Triple wire + Verus A23-A24
WAN P-M-C-R triple, dual multi-reply cover, CMR partial revoke, Verus A23-A24 mega composite. Not Tier 4 / not product SURB crypto.
Reverse Morph + dual SURB + birth
WAN reverse Morph (M-R), dual sequential SURB (P-R-R), dual birth+reply streams, Verus A25. Lab only.
Birth dual + reverse Cover + A26-A27
Verus A26-A27, multi-profile morph dual SURB, reverse Cover (C-R), CMR profile switch. Not Tier 4.
Multihop reverse Morph + dual-grant SURB
Multihop reverse Morph (M-R), dual-grant SURB isolation, birth+cover dual streams, Verus A28. Lab only.
Full CMBR dual + multihop Cover + A29-A30
Dual full CMBR, multihop reverse Cover (C-R), morph+birth+reply profiles, Verus A29-A30 mega. Not Tier 4.
Reverse triple M-C-R + dual-path SURB
Multihop reverse Morph+Cover+Reply, dual-path reverse SURB, CMBRC dual, Verus A31. Lab only.
Dual reverse replies + A32-A33
Multihop reverse dual Reply (R-R), morph+cover profiles, CMBR revoke+birth, Verus A32-A33 mega. Not Tier 4.
Reverse M-R-R + guest decoy
Multihop reverse Morph+dual Reply (M-R-R), Cover+dual Reply (C-R-R), guest decoy_tick (profile-required), dual decoy isolation, Verus A34. Lab only.
Decoy streams + dual-path Morph + A35-A36
Dual decoy+morph+cover+reply, dual-path reverse Morph, decoy+birth dual, Verus A35-A36 mega. Not Tier 4.
Multihop reverse Morph+Cover+dual Reply
WAN multihop reverse order M-C-R-R: Morph, Cover, dual SURB Reply through mid hop; single-use tokens, no ambient, revoke burn. Lab only; not product SURB crypto.
Verus A37 reverse M-C-R-R pure
Executable lemma discharge for pure order M-C-R-R (0=M,1=C,2=R) plus dual-reply count and compose A31/A34 rails. Not real Verus Tier 4.
Decoy revoke + DMCBR + reverse stretch
Dual-grant decoy/morph/birth revoke isolation, dual DMCBR (+ partial revoke), multi-profile decoy, WAN reverse M-C-R-R-R and C-M-R-R, Verus A38-A43 executable discharge. Lab only; not product SURB crypto or real Verus Tier 4.
Dual revoke family + reverse stretch wave
Thirty lab gates: dual-grant revoke isolation, multi-stream cocktails (DCR/CMDBR/CMDR/BMDR/DMCBR), multi-profile morph/decoy, WAN reverse M-C-M-R-R / C-M-C-R-R / M-M-C-R-R / C-C-M-R-R, Verus A44-A48 executable discharge. Not real Tier 4 or product SURB crypto.
Dual-path Cover+Morph + triple-grant slots
Dual-path reverse Cover+Morph WAN (Morph path + Cover path), GUEST_GRANT_SLOTS expanded to 3 with triple-grant decoy isolation, Verus A49-A50 executable discharge. Lab only.
Dual-path Morph+Cover co-order
Both reverse paths co-emit Morph then Cover then dual Reply (M-C-R-R) on distinct ports, with dual-grant SURB isolation. Differs from D197 split Morph-only / Cover-only. Lab only.
Dual-path co-order wave + triple-grant suite
Twenty lab gates: dual-path reverse co-order family (C-M-R-R, MCMRR, CMCRR, MMCRR, CCMRR both paths), GUEST_REPLY_SLOTS to 6, triple-grant morph/cover/reply/cocktail isolation, Verus A51-A57 executable discharge. Not Tier 4 or product SURB crypto.
Triple-reply co-order + quad-grant suite
Twenty lab gates: dual-path Morph+Cover+triple Reply (M-C-R-R-R) co-order, mixed and cross-order dual paths, GUEST_GRANT_SLOTS to 4 and GUEST_REPLY_SLOTS to 8, quad-grant isolation suite, Verus A58-A64 executable discharge. Lab only.
C-M-R-R-R both paths
Dual-path reverse Cover+Morph triple-reply co-order (C-M-R-R-R both paths) plus the C-M-R-R-R path primitive. Lab only.
Wave 50: order crosses + quad stretch
Fifty lab gates: remaining dual-path reverse order crosses (C-M-R-R-R x M-C-R-R-R first), 12 WAN labs, quad-grant isolation stretch (SURB exhaust, DMCBR, revoke, cocktail), Verus A65-A83 executable discharge. Lab only.
Product primitives: SiteId + onion SURB + Verus pin
SiteId fail-closed law on 127.0.0.1 vs 127.0.0.2, dual-site WAN and reconnect, 3-hop ChaCha20-Poly1305 SURB (replay/tamper/unlink), honest Verus pin crate (toolchain absent, A1 extracted, not Tier 4). Still one host.
Guest-path onion SURB
Host peels a 3-hop ProductSurb (ChaCha20-Poly1305), then kernel grant_tx binds the 16-byte id and consume-once charges the grant. Replay denied, revoke burns the handle. Not kernel AEAD unwrap. Not multi-machine WAN.
Two-process named-pipe WAN
Alpha parent and Bravo child are distinct OS processes over a local named pipe. SiteId still fail-closes cross-site. Same Windows user. Not a second NT account. Not multi-machine WAN.
One-hop peel yields payload
One-hop peel yields the payload. Host AEAD, not in-kernel ChaCha.
Two-hop order
Two-hop order is edge then dest. Host AEAD, not in-kernel ChaCha.
Three-hop id and body
Three-hop peel matches the SURB id and body. Host AEAD, not in-kernel ChaCha.
Tamper fail-closed
A tampered outer byte fails closed. Host AEAD, not in-kernel ChaCha.
Wrong hop key
A wrong hop key fails closed. Host AEAD, not in-kernel ChaCha.
Truncated wire
A truncated wire fails closed. Host AEAD, not in-kernel ChaCha.
Empty path rejected
An empty path is rejected. Host AEAD, not in-kernel ChaCha.
Nine-hop path rejected
A nine-hop path is rejected. Cap stays 8. Host AEAD, not in-kernel ChaCha.
Oversize payload rejected
An oversize payload is rejected. 1024 byte cap. Host AEAD, not in-kernel ChaCha.
Middle hop is not payload
A middle hop is not the payload. Host AEAD, not in-kernel ChaCha.
Dest cannot open outer onion
Dest cannot open the outer onion. Host AEAD, not in-kernel ChaCha.
Forward session unlink
A forward session cannot open the onion. Host AEAD, not in-kernel ChaCha.
Two seals differ
Two seals of the same payload differ (nonce). Host AEAD, not in-kernel ChaCha.
Consume refused until notes
Guest consume is refused until peels are noted. Does not open ciphertext. Kernel peel-count gate: consume waits for notes; still not in-kernel ChaCha.
Consume after three notes
Guest consume is ok after three notes. Kernel peel-count gate: consume waits for notes; still not in-kernel ChaCha.
Fourth note is excess
A fourth peel note is excess. Kernel peel-count gate: consume waits for notes; still not in-kernel ChaCha.
Consume replay
Consume replay stays consumed. Kernel peel-count gate: consume waits for notes; still not in-kernel ChaCha.
Revoke burns before notes
Revoke before notes burns the handle. Kernel peel-count gate: consume waits for notes; still not in-kernel ChaCha.
Peel count visible
Peel count is visible. Kernel peel-count gate: consume waits for notes; still not in-kernel ChaCha.
Composite peel
Composite peel covers consume, tamper, and unlink. Not multi-machine. Not Tier 4. Kernel peel-count gate: consume waits for notes; still not in-kernel ChaCha.
Showing the latest row only (most recent updates). Expand for D1 through earlier waves.
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
- Packet birth. External TX requires a live EgressGrant (or composed path grant). No grant means no packet.
- Cover bound to grant. Live grant implies cover charged to that grant's lifetime. Cover is not a free ambient presence channel.
- Trust is explicit. Peers are untrusted by default. Crypto and predicates, not ambient trust domains, authorize exchange.
Cover construction property
Cover is not ambient presence. It is a budgeted schedule charged to a live grant. While the grant lives, payload and/or cover cells may leave the domain. When the grant dies, cover ceases by construction so idle domains go quiet. That is a local construction property on host fabric paths, not a free win against a global passive adversary.
Diagram source (ASCII)
Fresh domain (zero net) -> No live grant -> wire: no domain-originated cells -> mint EgressGrant -> Grant live -> Cover charged to grant lifetime -> Payload and/or cover cells may leave -> REVOKE or expiry -> cover stops -> Idle quiet Lab OPEN/TICK/REVOKE exercises this; not a consumer API.
Adversary observation ledger
Observer class: local underlay / link observer (A-ISP class). Explicitly not end-to-end global passive adversary (A-GPA) confirmation.
| Domain state | What may leave | What observer may notice | What stops / residual |
|---|---|---|---|
| No grant | Nothing (no ambient TX, no cover beacons) | Silence on that fabric path | Other host/OS noise outside VeilNet may still exist |
| Live grant + cover | Payload and/or grant-bound cover cells | Presence of traffic; volume/timing shape of schedule | Raises idle fingerprint cost; does not erase timing classes |
| REVOKE / expiry | No new birth; cover scheduler stops | Traffic for that grant ends toward quiet | History already observed; other live grants may still emit |
VeilNet Lab Console
Interactive browser model of OPEN / TICK / REVOKE and timeline FORK / DISCARD / MERGE. Demonstrates the construction property: no external packet without a live grant; cover dies with the grant.
Browser simulation
Models D3/D5 public semantics
Not a live mesh / not a consumer API
Domain + wire
Domain
NoGrant
Cover
IdleQuiet
Budget
0
Timeline
Main
Fabric path (cells vs silence)
A-ISP class: silence on this fabric path (no ambient TX)
Event log
Try: OPEN then TICK several times, then REVOKE and watch silence. With this console focused, O, T, and R do the same. Or FORK, OPEN on the experimental world, DISCARD (or MERGE with HumanGate). TICK with NoGrant is always DENIED. Browser sketch, not a live mesh, not kernel AEAD.
Grant lifecycle
Lab control plane words OPEN / TICK / REVOKE (plus PING / HOST / SHUTDOWN on standing services) describe host fabric cover-daemon exercises. Not a public consumer API and not a production multi-host product.
Diagram source (ASCII)
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.
Diagram source (ASCII)
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 |
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
Diagram source (ASCII)
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 |
|---|---|---|
| 0 | rustc + cargo test | Active |
| 1 | Cap property tests | Active |
| 2 | Kani model checking | Scaffold |
| 3 | Verus-style hooks | Scaffold |
| 4 | Verus / Lean full proofs | Planned |
| 5 | seL4 substrate option | Design-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.
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, net TX+RX (DHCP/SLIRP lab)
- Legacy virtio fallbacks when modern path unavailable
Host fabric crates
- AetherIR -> hand JIT + CLIF interpret + CLIF native emit + optional real Cranelift JIT (feature)
- VeilNet grants + multi-hop path grants + cover scheduler
- WAN TCP multi-hop AEAD lab + multi-process cover daemon + standing process-per-host service lab (OPEN/TICK/REVOKE; grant survives reconnect)
- Timeline engine + twin shell surface
- Verification ladder + Verus-shaped invariant document
- Stub compositor / minifb GUI shell
- Guest-directed AEAD hop peel (D308-D327): host ChaCha opens each layer; kernel consume waits until peel notes match the hop count. ChaCha is not in the kernel image.
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
Aether: fs mount OK
Aether: fs write OK
Aether: fs read OK
Aether: elf load OK
Aether: elf exit=42
Aether: virtio-net modern TX OK
Aether: virtio-net modern RX OK
Aether: net app OK
Aether: grant-tx deny OK
Aether: grant-tx allow OK
Aether: grant-tx revoke OK
Aether: grant-tx sketch OK
Aether: verus lemma A1 discharged OK
Aether: verus lemma OK
Aether: multiport port1 data OK
Aether: console port1 OK
Aether: timeline cross-device OK
Aether: timeline grant hygiene OK
Aether: grant-tx cover quiet OK
Aether: grant-tx cover live OK
Aether: grant-tx cover OK
Aether: fabric-net deny OK
Aether: fabric-net allow OK
Aether: fabric-net OK
Aether: shell ready
Aether: shell session OK
boot OKWhere D328 starts
D308-D327 closed guest-directed hop peel in the host crate. D328, kernel-resident AEAD, is the next lab gate. It is not started and not green. The nav pill stays D327 | next D328.
Not started
Host ChaCha
Kernel counts notes
ChaCha opens each layer here. That is the lab-green part of D308-D327. It is not the kernel image.
Each hop is a layer. A 3-hop path needs 3 peels before the payload is the payload. The outer layer is not the message.
The kernel refuses consume until the peel count matches the hop count. Replay, revoke, a short wire, and an early consume still fail closed.
ChaCha is not in the no_std image. Putting AEAD there would be D328. That work has not started.
| Question | D308-D327 | D328 |
|---|---|---|
| Where the AEAD runs | Host crate | Would have to be inside the kernel image. Not started. |
| What the kernel does | Counts peel notes, then allows consume | No kernel-resident AEAD yet |
| Status | Lab green, 2026-09-21 | Not started. Not green. |
Still refused
This section does not claim multi-machine WAN, Verus Tier 4, a product appliance, or an ambition move. The bar stays about 35 percent of an 18 month personal-class estimate.
Fail-closed cases the peel lab already showed
Tamper, wrong key, truncated wire, empty path, oversize and 9-hop reject, replay, revoke, and consume before the note count matches. Those results belong to D308-D327. They are not D328.
What is coming
True remaining cliffs after the modern MULTI+FLUSH / CLIF / multi-hop / Verus-hooks wave. The next numbered lab gate is D328 (kernel-resident AEAD). N1-N4 stay open surfaces and are not the next Continuum number. 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
Planning horizon (~18 months) is at the top of the page, just under the hero. Jump to horizon - ambition bar, not a gate counter. Live data: /horizon.json.
Near (open surfaces)
D328 kernel-resident AEAD
ChaCha still lives in the host crate. D328 is the next lab gate: AEAD inside the no_std kernel image. Not started. The seam section on this page states the boundary. Not multi-machine WAN. Not Verus Tier 4.
cranelift-jit feature
Optional cranelift-jit feature wires real Cranelift (0.120). Quad parity lab green on pure arith demos. Default build stays light without the feature. Remaining: broader ops and product loaders.
Multi-host WAN standing service
Standing process-per-host cover service lab is green (shared grant across reconnect; two-host localhost). Remaining: production durability, supervision, routable WAN beyond lab. Not a consumer product.
Verus toolchain port
Invariants documented; hooks scaffold. Next is real proof fn discharge on a Verus toolchain.
Virtio-net + port1 data
Virtio-net modern first path is lab green under QEMU (DRIVER_OK + TX + RX via DHCP Discover / SLIRP Offer). Remaining: multiport port1 data queues, IRQ-driven RX, multi-buffer. Not a guest Fabric TX stack.
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.
Kernel-integrated VeilNet TX
Host Phase0 + multi-hop labs are green. Grant-bound egress inside the guest kernel / NIC path is not claimed.
Kani runnable CI (T2)
Kani-shaped harness intent exists as scaffold. Runnable green Kani CI is not claimed.
L1 agent swarm crates
Design + early host stubs only. Not a shipping local AI operator product.
L4 compositor beyond stub
minifb / stub compositor only. Living UI weaver is not a shipped product surface.
Personality / FS grant-only depth
IR + JIT live on host. Full multi-personality and HostSys FS grant demos remain deeper cliffs.
Cross-device timeline durability
Host fork / discard / merge paths are green. Cross-device timeline migrate is later phase, not claimed.
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.
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). See Cover construction and adversary ledger.
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 tests (Tier 0-1 Active). Continuum D1-D327 are lab-green observations, not machine-checked full proofs. D1-D5 are what feed that T0-T1 floor.
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.
Is AetherIR Wine or Rosetta?
No. Foreign binaries are intended to enter a capability host via AetherIR, not reimplement a foreign OS as architecture. See Runtime Fabric Codex.
What is proven on the runtime path today?
Host lab D2: hand JIT + CLIF interpret + CLIF native emit with parity demos. Full multi-format loaders and multi-personality HostSys are not claimed complete.
Is cranelift-jit shipping?
Not as a default dependency. Optional feature cranelift-jit wires real Cranelift with lab parity tests. Hand JIT + CLIF paths remain the default light stack.
Does cover defeat traffic analysis?
No free GPA defeat on public low-latency edges. Cover is grant-bound construction on host fabric paths: idle quiet when grants die. See the adversary observation ledger.
What is the next lab gate?
D328, kernel-resident AEAD. Lab depth is D1-D327. Ambition stays about 35 percent of an 18 month personal-class estimate. That is not a finished product.