Seal OS · Epsilon-Hollow

An operating system whose day job is machine learning.

OS state is topology on the unit sphere S². Training runs get a kernel that measures the shape of their overfitting. Inference gets a KV cache that evicts by elementary collapse.

  • bare-metal x86_64
  • UEFI
  • no_std Rust
  • own 69-call ABI today
  • next: the Linux kernel ABI
View on GitHub Read the README
The Seal OS seal, balancing the sphere its state lives on A seal sits upright and balances a glass sphere on its nose. The sphere turns slowly; on it sit the eight boot centroids, the cube vertices, and the three great circles that bound their Voronoi cells. The seal bobs gently and blinks.

Four things the kernel does that other kernels do not try.

Built to be the layer where a training run and an inference server are understood, not just scheduled. Each of these runs in the kernel today, on synthetic workloads; real-model validation is the open work.

A validation loss that falls and climbs back closes a loop in its delay embedding; one that only falls draws an open arc Two of stratum's test curves, drawn in turn. Left: the last 64 steps of the validation loss. Right: its delay embedding, the points (v_t, v_t−1, v_t−2) resampled at uniform arc length and drawn flat, with each axis scaled to fit, which is illustrative. The V, 0.3 + 0.01·|t − 100|, falls and climbs back. Each time the climbing arm comes within 1.68 times the largest spanning-tree edge of a point the falling arm passed, that Rips edge shuts the stretch of the run between them into a loop. 25 nested loops close, one after another as the run climbs, and loop_score is 25 / 64 = 0.391. The outermost stays drawn as a closed ring with arrows showing the way round it: down the falling arm, up the climbing arm, and back along the edge. The stretch of the run it spans is shaded on the loss curve. The exponential decay 0.05 + 0.55·exp(−t/22) only falls: its embedding is an open arc that never comes back, and loop_score is certified 0 before any complex is built. validation loss delay embedding loops and score by fold_score's rule; flat layout illustrative

stratum · Seal ABI 120–124

The kernel watches the shape of your loss curve.

Push (train_loss, val_loss) each step and get a regime back: Underfit, WellFit, Overfit or Collapsing. Overfitting closes a loop in the delay embedding of the validation curve. A run that only falls scores exactly 0. 4,792 bytes per stream, no allocation per sample.

Sequences share a prefix tree of KV blocks; a leaf no sequence uses is collapsed tree illustrative; the free-face rule is foliation's

foliation · Seal ABI 130–134

A KV cache that is a prefix tree.

Live sequences share cached blocks wherever their prefixes agree, and a sequence's block table is its path down the tree. Eviction removes only a free face: a block that is resident, unreferenced and has no resident children. Sharing requires an exact token match. Its eviction order matches the optimum on a trace built so that recency always evicts the shared prefix, and loses to LRU on a multi-turn chat trace, so the system-call cache defaults to LRU. Both traces, measured.

Frames and files land on the sphere and join the Voronoi cell of their nearest centroid each point joins its nearest centroid's cell

TopoRAM · ManifoldFS

Memory and files are points on a sphere.

Every physical frame carries 64 bytes of metadata: its S² embedding, access history, Voronoi cell and lifetime class. Files are placed and found the same way, by great-circle distance to Voronoi centroids, with spectral prefetch and an entropy governor over the cells.

A scale sweeps across merge heights; the count is certified between them and refused on them merge heights, log scale; band ratio 10

certify or refuse

It refuses rather than guesses.

Component counts, attention top-k, fit verdicts and nearest-centroid lookups come back with a certificate, or with a refusal naming the pair that made them ambiguous. The kernel does not return a number that rounding, not the data, chose. See every one drawn.

It boots · QEMU · OVMF

Ten theorem checks, one refusal, a desktop, an event loop.

The UEFI image boots under QEMU and checks T1 to T10 from aether_verified. T4 is judged at the step the governor actually runs, where its gain margin fails, so the line says NOT CERTIFIED and boot goes on; any other failure panics. Then the kernel brings up its layers, draws a desktop and enters its event loop. CI boots every build this way and fails it without the theorem, SealShell, desktop and event-loop lines.

9 / 10boot theorem lines VERIFIED 5.01T4's α + β/dt at the runtime dt of 0.01; certifying needs < 1 
$ qemu-system-x86_64 -machine q35 … seal-os.img
…
[T4/AGCR] Governor online: epsilon = 0.1000 alpha=0.01 beta=0.05 dt=0.01
…
[THEOREM] T1/TSS VERIFIED
[THEOREM] T2/SCM VERIFIED
[THEOREM] T3/GMC VERIFIED
[THEOREM] T4/AGCR NOT CERTIFIED: alpha+beta/dt=5.01 >= 1 at dt=0.01
[THEOREM] T5/HCS VERIFIED
[THEOREM] T6/RGCS VERIFIED
[THEOREM] T7/PHKP VERIFIED
[THEOREM] T8/TEB VERIFIED
[THEOREM] T9/CMA VERIFIED
[THEOREM] T10/WPHB VERIFIED
[BOOT] 9 of 10 theorems VERIFIED; T4/AGCR NOT CERTIFIED; T1-T3, T5 ACTIVE in runtime paths
…
[BOOT] Syscall FS ready
[BOOT] All layers initialized.
[Desktop] Rendering desktop environment
[SealShell] Loaded
[BOOT] Seal OS desktop ready.
[EVENT] Entering real event loop — keyboard and mouse active
Lines are the kernel's own format strings at 3c14df0, in boot order; "…" marks lines left out.

Accepted plan · 2026-09-27

Direction: a Linux kernel replacement.

Seal OS is to boot under any Linux distribution as that distribution's kernel: the userland runs unmodified, the bootloader and initrd tooling work unchanged, and Linux drivers are usable. Seven decisions carry it: the Linux x86_64 syscall ABI as the only ABI, the Linux boot protocol, Linux drivers unmodified inside isolated LKL driver servers, ext4 behind a crash-consistency gate that a stock Linux kernel replays, the geometric subsystems kept under Linux permissions, progress counted by the Linux Test Project, and pinned ports for whatever is not built natively.

0ring-3 instructions executed, with or without a /bin/init 1 / 49syscalls made by five Ubuntu programs that reach the same call 4,310of 4,310 scanned kernel pages writable and executable; 0 of 24,004 since b3cf934 853 / 924Linux driver modules the licence gate refuses in the kernel

The starting point, measured at 9ebbe2e; each number is a test under tests/linux_parity that fails there.

milestonescopegate, in QEMUstatus at c055594
M0ring 3; syscall entry on a kernel stack with swapgs; user faults kill the process; kernel W^X; ext2 feature refusal; theorem lines from live state; CI green; ports/chase_boot.sh usermode-seal, wx, ext4; ring3-seal; write(fd, 0x1000, 1) returns -EFAULTopen, 0 of 11 items closed; landed: kernel W^X (wx passes), T4 refused at boot, ports/ and PORTING.md
M1per-process address spaces, page cache, fd tables, SIGSEGVa boot-executed test per itemopen; gate not yet written
M2Linux ABI core: renumbering, six-argument dispatch, auxv, TLS, futex, clone, /dev/sealstatic glibc hello prints; busybox sh runs a scriptopen; ring3-glibc fails
M3Linux boot protocol, EFI stub, command line, initramfsGRUB loads Seal OS as linux to a busybox promptopen; gate not yet written
M4–M6Alpine without systemd; ext4 with jbd2; systemd distributionsAlpine to login; the crash-consistency gate; Debian, Ubuntu, Fedora and Arch to loginopen; gates not yet written
M7–M8ACPICA, ECAM, MSI, IOMMU, LKL driver servers; bare metalan unmodified Linux driver behind a virtual IOMMU; one reference machine to loginopen; ACPICA recorded as a planned port

docs/design/LINUX-REPLACEMENT.md

The plan

Starting point, decisions D1 to D7, milestone gates and what stays reversible.

Read the design

FUTURE_PLAN.md

Phase 0

One box per milestone and per M0 item, each ticked only when its gate passes.

See the boxes

PORTING.md

Porting

Where ported code may run, how it is pinned and licence-gated, and when a native implementation replaces it.

Read the rules

CONTRIBUTING.md

Contributing

A RED test first, and every theorem line certified, refused or not checked.

Start here

Every claim, drawn

Certify or refuse: the round that made the answers honest.

Eight results from the certify-or-refuse round, then eleven more ported from related work on 2026-09-27. Each one was a number that the arithmetic, not the data, had chosen. Each figure below runs the rule it describes.

1,215 → 0wrong nearest-centroid answers in 5,000 queries 0.96875 → 0loop score of a loss curve that only falls 0.001 → 10.0what one /mv did to ε; now it is held 849 / 0workspace tests passed / failed at 0f040e0
Eight boot centroids fold onto four and back The unit sphere with the eight Seal OS boot centroids, the cube vertices at colatitude acos(1/√3) and π − acos(1/√3), and their Voronoi cells, the eight octants. The centroids then slide to where the old code put them: placed by latitude ±asin(1/√3) and read as colatitude, where (−t, φ) is (t, φ + π), all eight land on one ring in four coincident pairs. The minimum separation, computed live, drops to 0 against T1's θ_min of 0.50536 and the T1/TSS line fails. They slide back, the separation returns to acos(1/3) = 1.2310, and the boot line reads VERIFIED. colatitude acos(1/√3), π − acos(1/√3): the cube placed by latitude, read as colatitude: eight on four θmin 0.50536 0 0.5 1.0 minimum centroid separation 1.2310 rad [THEOREM] T1/TSS VERIFIED [THEOREM] T1/TSS FAILED
The separation is measured on the drawn centroids every frame.

01 · T1/TSS · b9a4531

The boot stopped failing its own theorem.

The eight boot centroids were placed at latitude ±asin(1/√3), but the distance reads colatitude, where (−t, φ) is (t, φ + π). Eight centroids fell onto four, T1 measured a minimum separation of 0 against θmin 0.50536, and boot panicked. At colatitude they are the cube again, 1.2310 rad apart, pinned by a compile-time assert because seal-os tests do not run.

0minimum separation, before acos(1/3)minimum separation, after
How it was checked, 3 ways
  • locate over the cube returned [0, 1, 2, 3, 2, 3, 0, 1] before and [0 … 7] after
  • ManifoldMemory::great_circle had the same latitude formula: two equator points a quarter turn apart measured 0 (73372ac)
  • a QEMU boot of the release image prints [THEOREM] T1/TSS VERIFIED
A nearest centroid across the pole, missed and then found A view down onto the north pole of the grid-hash index with two centroids, so the grid has 4 colatitude rows and 8 longitude columns. The query sits at colatitude 0.1, longitude 0. Slot 0 sits at colatitude 0.1, longitude 3.0, just across the pole, 0.1995 rad away. Slot 1 sits at colatitude 1.0, longitude 0, 0.9 rad away. The old 3 by 3 block around the query is a wedge that stops at the pole, so it held only slot 1 and returned it. The fixed block takes every column once it touches a pole row, a polar cap, and returns slot 0. slot 0 slot 1 query pole at the centre, colatitude out to 1.2 before the 3×3 block is a wedge that stops at the pole slot 1, 0.9 rad away now a block on a pole row takes every column slot 0, 0.1995 rad away
Centroids and query are the test's pole counterexample.
The same 5,000 queries before and after Two bars of 5,000 seeded queries against 8 centroids. Before: 3,785 answers were the true nearest centroid and 1,215 were not, and the index reported a hit rate of 1.0000. After: 4,909 answers are certified inside the 3 by 3 block and 91 queries scan every centroid; none is wrong, and the reported hit rate is 0.9818 because it counts only certified answers. before 1,215 wrong 3,785 right; reported hit rate 1.0000 after 0 wrong 4,909 certified in the block, 91 scanned in full reported hit rate 0.9818: only certified answers count
Before: commit cdb4a4e. After: probe_e re-run at 0f040e0.

02 · grid-hash locate · cdb4a4e

A lookup that never checked outside its block.

SphericalGridHashIndex::locate returned the best centroid in the 3×3 cell block around a query and counted it as an O(1) hit. Nothing checked for a nearer centroid outside the block, and the block was a wedge even at the pole. It now accepts the block winner only when it is nearer than any point outside the block can be, and scans every centroid otherwise.

1,215wrong of 5,000, before 0wrong of 5,000, after
How it was checked, 3 ways
  • 25,000 seeded queries over K = 2, 8, 20, 64 and 200: 101 of 5,000 wrong at K = 2 before, 0 wrong at every K after
  • the pole counterexample returned slot 1 before and slot 0 after
  • an equatorial query whose block winner is 1.47 rad away against a 0.785 rad boundary reported a hit rate of 1.0 before and 0.0 after
Sixteen points, their spanning tree and the band around the scale Sixteen points in the plane: three tight clusters and one loose point. Their minimum spanning tree is drawn above a log axis of its merge heights, with the band from s/√10 to s·√10 around the scale s. Tree edges below the band are merged and drawn in blue, edges inside it in coral, edges above it faint green. When no height sits in the band the count of components is certified; otherwise the count is refused and the in-band edge nearest the scale is ringed. The slider moves s. 0.001 0.01 0.1 1 spanning-tree merge heights, log scale; band ratio 10 β₀
The points are chosen for the picture; the tree, the band and the verdict are computed by the rule.

03 · certified β₀ · 8678c97

A component count is certified, or the pair is named.

certified_beta0 takes the n − 1 merge heights of a Euclidean minimum spanning tree. If none lies in [s/√10, s·√10], every threshold in that band gives the same count and it is certified. Otherwise the answer is a refusal naming the edge nearest the scale. The seal-os encoder used to count at a chord of 0.5 with a strict <. It now stores the certified count, or u32::MAX.

0.5 ± 1e-9chord pair: two integers before, both refused now 500seeded clouds agree with all-pairs union-find
How it was checked, 4 ways
  • permutation, isometry and scale invariance; a single point, an empty cloud, a non-finite coordinate
  • heights use m·√Σ(d/m)², so a 1e-170 separation no longer squares to zero and 1e170 no longer overflows
  • 30 embeddings, seed 42: a spanning edge of 0.089 at ε = 0.1 was accepted, and is now refused (cb8a873)
  • planted mutants (h <= lo, h >= hi, clamp removed, wrong edge named) each fail a test
Six scores as intervals, a budget of two, and the boundary between them Six keys, each score drawn as an interval of the rounding radius around its float value. The budget is two. The two float leaders are kept only when both of their lower ends clear every other key's upper end; the dashed line marks the lowest selected lower end. When an unselected interval reaches it, the row widens to every such key, drawn amber. With one score overflowed to NaN, the row refuses and falls back to dense over all six keys. The slider sets the radius. 0 0.5 1
Scores and radii are illustrative; the keep, widen and fall-back rule is certified_top_k's.

04 · attention top-k · afd0969, eb4af16

Top-k keeps its keys only when the intervals separate.

Each score carries Higham's a-priori bound γₙ·Σ|q_d k_d|. The top set is kept only when every selected lower end clears every unselected upper end. Otherwise the row widens to every key that reaches the lowest selected lower end, at no extra dot products. A NaN or infinite score refuses, and the row falls back to dense.

0.0 vs 1float vs exact score of k₀ = [1e17, 1, −1e17] at q = [1, 1, 1] 2tests in the workspace suite that widen any row: the two counterexamples
How it was checked, 3 ways
  • on that q and k, OracleTopK{budget: 1} took key 1 (0.5) over key 0 (exact 1)
  • each test carries its exact reference: i128 for the inflated score, u128 for the radius against γ₈
  • 2·1e308 + 2·(−0.95e308) reads NaN; such a row refuses as TopKRefusal::NonFinite and is listed in dense_rows
A loss curve, its delay cloud, and the loops the cloud closes Left: the last 64 steps of a validation loss. Right: its delay cloud, the points (v_t, v_t−1, v_t−2) resampled at uniform arc length and projected flat, with every Rips edge at 1.68 times the largest spanning-tree edge. Path edges are grey, two-step chords that a Rips triangle fills are dashed, and edges that close a loop are coral. A clean V, 0.3 + 0.01·|t − 100|, folds back on itself and scores 0.391. A staircase that only falls scored 0.96875 under the old reading at margin 1.5, where every corner closed a triangle. Now a monotone window is certified 0 before any complex is built. validation loss, last 64 steps delay cloud, projected
The loop score is computed live by a port of fold_score that reproduces 0.391 and 0.96875.

05 · stratum · abc7e0f, d52f6c6, dbbce44

A loss curve that only falls scores exactly zero.

stratum watches a training run's validation loss and counts loops in its delay embedding: overfitting folds back, a healthy run does not. A staircase turns by up to 90° at every change of slope, each corner closed a triangle, and the run was called Overfit. fold_score now checks monotonicity in O(n) and returns a certified 0. Two-step chords that a triangle fills are no longer counted, and the margin is 1.68, inside the derived band (1.633, 1.732).

0.96875staircase loop score, verdict Overfit, before 0certified, before any complex is built
How it was checked, 3 ways
  • the Underfit fixture scaled by 1e-3 read spread 1.0 and WellFit, against 0.3529 and Underfit at ×1; the ratio now agrees within 1e-9 from 1e-300 to 1e300
  • a refused spread withholds only the Underfit gate; it no longer forces Collapsing
  • mutants at margins 1.0, 1.3 and 1.8 each fail a host test
Two sequences in the prefix tree, a key collision, a collapse and a refusal A prefix tree of cached KV blocks. Sequence A descends from the root through block 1 to a leaf keyed 0xe0e00501162145bc. Sequence B has different tokens whose key collides. Before, B shared A's leaf and read its KV state. Now the tokens are compared and B gets its own leaf. When B releases, its leaf is resident, unreferenced and childless, a free face, and it is collapsed. Then a task that did not open sequence A tries to release it and is refused with NoSuchSeq.
The tree is a sketch; the key is the collision pinned in the kernel's const assertion.
Hit rates of four eviction policies and the Belady optimum on two traces Hit rates in basis points, measured under QEMU with the same 24-block pool, on one common axis from 0 to 10,000. Boot trace, where the shared prefix returns only after 31 other blocks: Belady 952, foliation 952, the locality-only null 476, LRU 0, random 238 to 857 over 32 seeds. Chat trace, 4 live conversations served round robin, where reuse follows recency: Belady 8,143, foliation 5,284, the locality-only null 6,818, LRU 8,068, random 7,026 to 7,443 over 32 seeds. Foliation matches the optimum on the first trace and comes last on the second. boot trace: foliation matches Belady the shared prefix returns after 31 other blocks; the pool holds 24 Belady (optimum)foliationlocality-only nullLRUrandom, 32 seeds Belady (optimum)foliationlocality-only nullLRUrandom, 32 seeds boot trace, Belady: 952 bp boot trace, foliation: 952 bp boot trace, locality-only null: 476 bp boot trace, random over 32 seeds: 238 to 857 bp chat trace: foliation comes last 4 live conversations, round robin; reuse follows recency chat trace, Belady: 8,143 bp chat trace, foliation: 5,284 bp chat trace, locality-only null: 6,818 bp chat trace, LRU: 8,068 bp chat trace, random over 32 seeds: 7,026 to 7,443 bp 9529524760238–857 8,1435,2846,8188,0687,026–7,443 02,5005,0007,50010,000 hit rate, basis points; 10,000 means every descent hits
Measured under QEMU. Boot trace: CI run 36165748105, locality null 264235c. Chat trace: 0ab2377, random range from a host replay.

06 · foliation KV cache · 98b023b, 659c376, 90aa07e, 0ab2377

The KV cache shares a block only when its tokens match.

foliation shares a cached block between sequences with the same prefix. It shared whenever a 64-bit fold_key matched and never compared tokens, so two different blocks could read each other's KV state. A leaf now stores its tokens. Eviction only ever collapses a free face, and a task that did not open a sequence gets NoSuchSeq from SYS_KV_SEQ_APPEND, _RELEASE and _STATS. Which free face to collapse is another matter: the foliation ranking matches the optimum on a trace built so that recency always evicts the shared prefix, and comes last on a multi-turn chat trace.

952 bpboot trace: foliation, equal to Belady; LRU scores 0 by construction 5,284 bpchat trace: foliation, against LRU's 8,068; it beats 0 of 32 random seeds
How it was checked, 4 ways
  • the collision 0xe0e00501162145bc was found by meet-in-the-middle against the shipped function and is pinned by a const assertion
  • the ABI default is LRU: with 16 live conversations instead of 4 the chat result reverses, 5,113 bp against LRU's 3,731 (one mutation build), so the winner follows whether reuse distance exceeds the pool
  • a locality-only null, the ranking without its entrant count, scores 476 bp on the boot trace and 6,818 on the chat trace; --check-kv-policy requires both traces (40d3568)
  • a foreign release, append and stats read are refused while the owner's blocks stay referenced
The T4 gain margin against the tick period, and a run whose error grew Top: the gain margin α + β/dt for α = 0.01 and β = 0.05, on log axes, against the line at 1 below which T4 certifies. At dt = 1 the margin is 0.06 and certifies. At the runtime tick dt = 0.01 it is 5.01 and does not. The slider moves dt. Bottom: the error of a governor run at α = 0.001, β = 0.05: 0.1, then 0.0959612, then 0.0960443. It rises at step 2, and verify_theorem now refuses the run there. 0.01 1 tick period dt, log scale α + β/dt |e| per step, α = 0.001, β = 0.05 rises at step 2: refused it ended inside the rate window and used to be certified
The margin curve is the formula; the three |e| values are quoted from commit 6c450d4.

07 · governor, T4/AGCR · c5b5853, 6c450d4, 2605f70, 3c14df0

The governor stopped certifying runs that did not converge.

epsilon-os checked T4 at boot with dt = 1, while the governor ticks at dt = 0.01, where the margin is 5.01. The READY line now says T4 is not active, and the seal-os boot gate now refuses T4 the same way. verify_theorem certified runs whose error stalled or grew, and now refuses at the first step that does not contract. /mv ran two ticks whose derivative spike threw ε from 0.001 to 10.0. It now runs none.

70 → 12of 420 configurations still certified 5.01α + β/dt at the runtime dt; certification needs < 1
How it was checked, 4 ways
  • a run with ε pinned at 0.1 holds e = 1.7 at every step; it was certified and is now refused at step 1
  • ε and the tick count are pinned bit-identical across one /mv
  • boot prints [READY] Manifold filesystem online. Not active: T4/AGCR NOT CERTIFIED.
  • seal-os boot prints [THEOREM] T4/AGCR NOT CERTIFIED: alpha+beta/dt=5.01 >= 1 at dt=0.01, and --check-theorem-log rejects a VERIFIED line at that margin; with the gate put back at dt = 1, the in-kernel harness passes 563 of 564 and the log gate fails (3c14df0)
A full cell splits, and some files become unreachable Sixty-five files arrive in one Voronoi cell, placed along the split axis by their coordinate. The cell holds 64, so the 65th insert splits it at the mean. Before, the split sent each file to a side by a hash of its inode id, while lookups routed by its coordinate against the same boundary, so every file whose two sides disagree, ringed coral, could no longer be found. Now split, insert, lookup and removal all route by the same point, and every file is reachable. coordinate on the split axis
Positions and hashes are drawn at random; the split and routing rules are voronoi_cap's.

08 · ManifoldFS cells · 8e378e8, f00e8f9

Split, lookup and removal route by the same point.

VoronoiCap::split_cell sent a file to a side by a hash of its inode id, a value in [0, 1], while locate routed by its first coordinate, a value in [−1, 1], against the same boundary. After the 65th insert into a cell, find could miss a file stored before the split. Every id now records its point, and all four operations route through one function over it.

64files a cell holds before it splits 520payloads the test inserts, 8·64 + 8, so some cell always splits
How it was checked, 3 ways
  • every id is exactly once in its locate() bucket after a split and after removing every subcell-1 id
  • a T3 entropy merge now redirects lookups to the merged cell; every file is found after entropy passes 2.0
  • voronoi_cap::basic_insert_locate is now registered with the runner; it had never run

Imported · 2026-09-27

Eleven fixes ported from related work.

Each port started from a test that failed for the reason in the "before" column and passes after it. The numbers are quoted from the commit that landed each one; all eleven are in the table in docs/RESULTS.md with their test counts.

fromrule portedwherebeforeafter
cleaveunion-find join: the absorbed root points at the survivorcut_tree, aether-corepoints [0, 1, 10] cut at k = 1 gave two clustersone cluster (14a3bb1)
cleavethe same joinentropy merge, epsilon-os ManifoldFSa file stored after a merge landed in the emptied cellrouted to the survivor (82e034f)
resolventrefuse non-finite logits before the softmaxscheduled_attention, aether-coreq = [1e200], k = [-1e200] returned Ok([NaN])NonFiniteScore at row 0, column 0 (c26d88a)
resolventthe same refusal, in the reference kernelssparse_attention, dense_masked_attentionthe dense reference answered Ok([NaN]) where scheduled_attention refusedboth refuse (af416fa)
sigmoidChebyshev keep: σ from the scores judged; no spread, no pruningregulate_entropy, aether-core heap64 of 64 objects pruned in one pass, against a proved ceiling of 16within the ceiling (f20f6b2)
separatrixdecide d < ε only where the error interval clears εrips_betti_1, aether-coreunit square at ε = fl(√2): β₁ = 1, exact 0refused, naming pair (0, 2) (82e4a8f)
separatrixcertify a pair only where d − R > θmin, R the rounding radiusverify_separation, aether-core and aether_verifieda pair 0.4999995 apart at θmin = 0.5, and a NaN pair, were certifiedboth refused (2014ddb)
branchcutan injective map onto m values misassigns at least n − m; checked to be 08-cell index of the scheduler, compositor and firewallslots 3 and 6 unreachable: locate gave [0, 1, 2, 0, 4, 5, 0, 7][0 … 7], on the cube (87d7b10)
branchcutthe same certificate, for the routerroute index, seal-os network5 distinct slots of 8; a lookup searched only its own cell and missed a route 0.08 rad away[0 … 7], and the nearest route over every cell (9702061)
triton-lang/kernels#22sink plus local window, used as a nullPolicy::Locality, foliationno replay separated the entrant term from depth476 bp against foliation's 952 on the boot trace (264235c)
NeMo-Relay#481a stable scaffold under varying turnschat trace, foliation proofthe proof replayed only a trace LRU loses by constructionfoliation 5,284 bp against LRU 8,068 (0ab2377)

One test, four questions.

Compute the answer with an enclosure. If the enclosure stays clear of the decision boundary, return the answer. If it touches the boundary, return the witness, and let the caller widen, scan or refuse.

questioncertified whenotherwisecaller then
β₀ at scale sno spanning-tree merge height lies in [s/√10, s·√10]refused, naming the edge (i, j, height) nearest sstores u32::MAX, or rejects the payload
top-k of q·kevery selected lower end exceeds every unselected upper endBoundaryRefusal: both keys, the float gap, the margin neededwidens the row, or falls back to dense
fit of a training runa monotone window scores 0; the spread clears a relative rounding boundthe participation ratio is NaNwithholds the Underfit gate only
nearest centroid on S²the block winner is nearer than any point outside the block can beno answer from the blockscans every centroid

Limits.

All of them, in one place.

  • No user program has run

    No ring-3 instruction has executed. /bin/init is absent from the image; with one present, boot stops after [execve] Loading '/bin/init'. Syscall entry stores onto the caller's stack. Everything on the desktop, the shell included, is kernel code. Reaching ring 3 is milestone M0 of the Direction.

  • Kernel tests do not run on the host

    kernel/seal-os is excluded from the Cargo workspace, so its #[cfg(test)] tests are never compiled or run. Kernel checks run only in the in-kernel harness and the seal-mkimage boot proofs under QEMU, and the harness job fires only after CI succeeds. That is why several seal-os fixes here are pinned by compile-time assertions.

  • Synthetic results are screening only

    stratum's fixtures and foliation's two traces are synthetic, and nothing has been run against a real model. Which eviction order wins follows the trace: foliation matches the optimum where recency always evicts the shared prefix, and loses to LRU, 5,284 bp against 8,068, where reuse follows recency. With 16 live conversations instead of 4 it wins again. Both traces run at one pool size.

  • T4 is refused, and no step size earns it

    epsilon-os and the seal-os boot both report T4/AGCR NOT CERTIFIED at the governor's runtime dt = 0.01, where α + β/dt = 5.01. The margin assumes unit plant gain; the loop the code runs has a gain of about 10⁶ and 2-cycles between ε = 0.001 and 10 at dt = 0.01, 0.0506 and 1 alike (dcc35b6). The governor needs a redesign, not a new dt.

  • A certificate covers the question as posed

    It says rounding and the choice of threshold cannot change the answer. It says nothing about whether the scale, the ratio of 10 or the embedding on S² was the right question. The points, scores and trees in figures 3, 4, 6 and 8 are chosen for the picture; the rules applied to them are the code's. The hit rates in figure 6 are measured, not chosen.

  • Elsewhere in the kernel

    From the Limits in docs/RESULTS.md: TLS accepts Ed25519 certificates only; AMD GPU dispatch has never executed; WiFi and Bluetooth are PCI probes only; KASLR moves mappings, not the image base; 611 of the kernel's 627 unsafe blocks carry no safety comment. Kernel W^X is now enforced, with 0 of 24,004 scanned pages writable and executable (b3cf934).

  • Where the numbers come from

    Every "before" figure is quoted from the commit named beside it. The nearest-centroid "after" figures, the stratum scores and the workspace count were re-run at 0f040e0 on Windows 11 with rustc 1.97.1: cargo test --workspace passed 849, failed 0, ignored 2. The 2026-09-27 results are quoted from the commits named beside them; at c055594, cargo test -p aether-core -p epsilon-os passed 490, failed 0. The QEMU results are quoted from the commits.

Reproduce it.

The host suite on stable Rust, the kernel on nightly for the UEFI target, and the boot under QEMU as .github/workflows/ci.yml runs it.

1. Host workspace

Everything except kernel/seal-os, which the workspace excludes.

cargo test --workspace
cargo test -p aether-core --test wf_tss_s2_index_probe probe_e -- --nocapture
# queries=5000  voronoi!=grid: 0  grid!=true-nearest: 0
# grid o1_hit_rate reported = 0.9818
cargo test -p aether-core --test certified_betti --test trajectory_shape --test attention_contracts

2. Kernel, nightly, UEFI

Needs the rust-src and llvm-tools-preview components. --features test-mode builds the image that runs the in-kernel harness.

rustup component add rust-src llvm-tools-preview --toolchain nightly
cd kernel/seal-os
cargo +nightly build --release
cd ../seal-mkimage
cargo +stable run --release        # writes seal-os.img next to seal-os.efi

3. Boot under QEMU and check the theorem lines

OVMF firmware, one AHCI disk, serial to the terminal.

timeout 240 qemu-system-x86_64 -machine q35 -cpu qemu64,+rdrand \
  -drive if=pflash,format=raw,readonly=on,file=/usr/share/OVMF/OVMF_CODE_4M.fd \
  -device ahci,id=seal_sata \
  -drive if=none,id=seal_disk,file=kernel/seal-os/target/x86_64-unknown-uefi/release/seal-os.img,format=raw,media=disk \
  -device ide-hd,drive=seal_disk,bus=seal_sata.0,unit=0 \
  -nographic -m 4G -no-reboot -no-shutdown | tee /tmp/seal-os.log
cargo +stable run --manifest-path kernel/seal-mkimage/Cargo.toml --release -- --check-theorem-log /tmp/seal-os.log
# expect: [BOOT] 9 of 10 theorems VERIFIED; T4/AGCR NOT CERTIFIED; T1-T3, T5 ACTIVE in runtime paths