CSpace / caps
Capability table entries. Rights are explicit slots, not ambient process privileges. SerialWrite isolation demo: A ok, B denied.
Project 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.
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.
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.
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 as of the last kernel + host wave. Green means observed under test or QEMU serial, not marketing.
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.
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. Or FORK, OPEN on the experimental world, DISCARD (or MERGE with HumanGate). TICK with NoGrant is always DENIED.
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
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 OKWhat 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
Planning horizon (~18 months)
Visual estimate of the road ahead. Lab boot under QEMU is already green. Bars are ambition bands, not promised ship dates. Focus and funding shift the calendar.
Now: lab bootable
Estimate only
Lab bootable
QEMU/UEFI freestanding boot, D1-D5 green, virtio + host fabric labs. Already shipping evidence on this map.
Done under QEMUInteractive appliance
Shell residency + mini FS lab green (D6-D7). Next: load userspace ELF (D8), net app path (D9). Feels like a tiny OS in QEMU.
D6-D7 lab greenArchitecture depth
Guest VeilNet TX path, Verus climb, agent swarm crates, compositor beyond stub, personality/FS depth, richer net and timeline durability.
Mid cliffsPersonal-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.
Near (ship order)
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 / 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.
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.