Epsilon-Hollow

What it is

Epsilon-Hollow is the repository; the kernel inside it is called Seal OS. It is a research kernel for x86_64, written in no_std Rust and booted only as a UEFI application. A conventional kernel measures its workload by quantity: resident pages, CPU time, open files, queue depth. It keeps no model of the workload’s shape. To Linux, a training run is a process with a large heap and an inference server is a process with a larger one. Whether the run is converging or memorising its training set, and which prefixes live conversations share, are facts the kernel could compute and never does.

Seal OS starts from the other end. Physical frames, files and tasks are placed on the unit sphere $S^2$ as points or small point clouds, each owned by the Voronoi cell of its nearest centroid, and placement and prefetch are read off that geometry. A trainer hands the kernel two numbers per step, and the kernel names the regime the run is in from the shape of its validation curve. An inference server’s KV cache is a prefix tree in kernel memory.

Shape comes back as integers: how many components, which $k$ keys, which cell, whether a curve folds back on itself. Those integers are computed in floating point, and near a decision boundary “the rounding of the arithmetic, not the data, picks the answer.” So the kernel holds itself to one rule. It computes an enclosure of the quantity. If the enclosure clears the boundary, the answer leaves with a certificate. If it touches the boundary, the answer is a refusal that names the witness, and the caller widens, scans or gives up.

The rule binds the kernel’s own claims too. At boot the kernel evaluates ten theorem lines, T1 to T10, against the values its running subsystems were built from. The code at commit 36b1400 prints one verdict per line, CERTIFIED, NOT CERTIFIED or NOT CHECKED, and a tally. CI greps for this tally, and seal-mkimage --check-theorem-log recomputes it from the ten lines:

[BOOT] Theorems: 2 certified (T1/TSS T2/SCM), 1 not certified (T4/AGCR), 7 not checked (T3/GMC T5/HCS T6/RGCS T7/PHKP T8/TEB T9/CMA T10/WPHB)

The README and docs/THEOREMS.md still quote an older banner, “9 of 10 theorems VERIFIED”; the code is stricter than the docs, and I follow the code. T4 is the governor’s convergence claim, and the kernel refuses it at the step the governor actually runs. Seven of the ten lines are not checked at all, because the kernel has no running instance of what each one describes.

What the kernel is not matters as much. No instruction has executed in user mode; the applications are kernel code. Bring-up of the other processors is written, but its only call is commented out. Hardware coverage is one QEMU configuration. So I do not describe Seal OS as a general operating system. It boots under QEMU, brings up its drivers, mounts its filesystem, replays its ML proofs on synthetic traces and evaluates its own theorem lines, and those are the parts this essay is about.

One tool grew out of this work: separatrix, which has its own essay.

What it can do

The README names four pillars, and says of them: “Each runs in the kernel today, on synthetic workloads. Validation on real models is the open work.” CI numbers below are from run 36165748105 on commit 9ebbe2e, the run in which CI is red (see Limitations).

stratum: a training run has a shape

A trainer passes (train_loss, val_loss) once per step through system call 121 (SYS_FIT_OBSERVE); call 122 (SYS_FIT_REGIME) returns Underfit, WellFit, Overfit or Collapsing. The kernel sees nothing else of the model: no weights, activations or gradients. Non-finite input is counted and latched, never used.

The test is geometric. The last 64 validation losses become delay points $p_t = (v_t, v_{t-1}, v_{t-2})$. A run that only falls draws an open arc. A run that falls and then climbs back through values it already visited draws a V, and at a large enough scale the two arms of the V close into loops. In the README’s words: “Overfitting is revisitation, and revisitation is a cycle.” The construction is in How it was made.

The verdict is advisory. The FitAction documentation says so directly: “Every field is advisory today, and nothing here is enforced against a task that ignores it.” SYS_FIT_REGIME publishes a prefetch threshold, and the only reader of that threshold is a prefetch preset that, in the source’s words, nothing constructs. The figure below runs the same classifier on a curve you paste.

foliation: an inference cache is a prefix tree

A sequence’s block table is its path down a prefix tree the kernel holds. A block is 8 tokens; each resident block is one 4 KiB physical frame from the kernel allocator. Two sequences that agree on a block-aligned prefix land on the same blocks, and there is no call to share a block: appending identical tokens does it. The source says it plainly: “Prefix sharing is not a hash table bolted onto an allocator.” A 64-bit digest of the prefix narrows the search, and a child is shared only when the token array also matches, because the digest can collide.

Eviction may remove only a free face: a block that is resident, unreferenced, and has no resident children. The resident set therefore stays a connected rooted subtree under every policy, and policies differ only in which free face they pick. The foliation policy picks the leaf fewest sequences ever entered, then the deepest, then the oldest.

The repo measures it on two synthetic traces at a 24-block pool, with “bp” meaning basis points of descents that hit a shared block:

That trace is built so that recency always evicts the shared prefix: the hot prefix returns only after 31 other blocks, more than the pool holds, and a const assertion in the source states the construction. LRU’s 0 is a property of the trace. On a multi-turn chat trace, where reuse follows recency, the result flips:

With 16 live conversations instead of 4, one mutation build reverses it again (5,113 bp against LRU 3,731 and Belady 5,378). The repo’s reading is the one I hold: “Which policy wins follows whether reuse distance exceeds the pool, not the name of the request shape.” Because of that, the cache behind the system calls defaults to LRU, and the source comment at its constructor says the foliation ranking “beats LRU only at a capacity cliff on the synthetic boot trace and ties or loses elsewhere.”

Certify-or-refuse, before and after

The matching rows for component counts and attention top-k sit next to their equations in How it was made.

TopoRAM and ManifoldFS: state on a sphere

Every physical frame carries an embedding of 16 points on $S^2$ (32 quantized angles, 64 bytes), a 64-tick access history, a Voronoi cell and a lifetime class. Memory is split into three zones, each with eight seeds; a frame belongs to the cell of its nearest seed.

ManifoldFS encodes a file’s bytes as a point cloud on $S^2$ and files the inode in the Voronoi cell of the cloud’s first point; the bytes persist through ext2.

The README adds the sentence that has to go with both numbers: “Whether this layout beats a conventional allocator or filesystem has not been measured; no comparison against Linux exists.”

Upstream

Work on Epsilon-Hollow led to these fixes in two other projects. I state the link in those words and no more.

landed in openxla/xla #46539 · commit 3d5df1d

fix(gpu): make reduction group order deterministic

Switches the set that drives the union-find merges in GroupDisjointReductions to absl::linked_hash_set, so the group-to-block assignment no longer depends on hash-set iteration order (as the PR states it).

Work on Epsilon-Hollow led to this fix.

openxla/xla #46539teerth.dev/openxla-46539

merged into tensorflow/tensorflow #124410 · 2026-08-05

Fix transitive reduction of collective control edges

Closes reachability exactly in one pass, so the unique transitive reduction of the collective control edges is emitted; the PR's four-op example drops a redundant edge (four edges to three).

Work on Epsilon-Hollow led to this fix.

tensorflow/tensorflow #124410teerth.dev/tensorflow-124410

How it was made

The kernel is one no_std crate, kernel/seal-os, built for x86_64-unknown-uefi. Drivers, filesystems, the network stack, the window manager and the applications compile into one EFI image. The mathematics lives in a workspace crate, aether-core: certified $\beta_0$, certified top-k, trajectory shape, the spherical Voronoi indices, the governor. The kernel calls into it. I follow the repo’s own numbered equations, (1) to (9), then the Lean files, then the paging that holds it all.

Certified β₀

Let $h_1 \le \dots \le h_{n-1}$ be the edge weights of the Euclidean minimum spanning tree of a point set $X$; these are exactly the single-linkage merge heights. The number of components at threshold $t$, and the condition under which a count at scale $s$ with band ratio $r \ge 1$ is certified, are:

Every threshold in the band, under < or <=, gives the same integer, which is what the certificate means. If a height lies in the band, the result is Refused { i, j, height }, naming the in-band tree edge whose height is nearest $s$. Heights are computed as $m\sqrt{\sum_d (\delta_d/m)^2}$ with $m = \max_d |\delta_d|$, so separations near $10^{-170}$ or $10^{170}$ neither underflow nor overflow. certified_beta0 builds the tree with all-pairs Prim, $O(n^2)$. The rule is ported from planimeter’s gap rule.

Certified attention top-k

Each score $\hat{s}_j = \mathrm{fl}(q \cdot k_j)$ of head dimension $n$ carries Higham’s a-priori bound for a floating-point inner product (Accuracy and Stability of Numerical Algorithms, Chapter 3; the repo cites it as Theorem 3.1):

The absolute value sits inside the sum. The source comment is specific about why: “gamma_n · |q·k| is not this bound and is far below it under cancellation, which is exactly where it matters.” The computed radius inflates (3) by $(1 + 2\gamma_n + 4u)$, adds $n$ times the smallest subnormal, and rounds up, so it bounds rather than estimates:

// kernel/epsilon/epsilon/crates/aether-core/src/attention.rs:885-898 @ 36b1400
fn enclosed_dot(q: &[f64], k: &[f64], i: usize, j: usize, head_dim: usize) -> (usize, f64, f64) {
    let (mut sum, mut magnitude) = (0.0f64, 0.0f64);
    for d in 0..head_dim {
        let product = q[i * head_dim + d] * k[j * head_dim + d];
        sum += product;
        magnitude += product.abs();
    }
    let n = head_dim as f64;
    let u = f64::EPSILON / 2.0;
    let gamma = nextafter(n * u / (1.0 - n * u), f64::INFINITY);
    let underflow = n * f64::from_bits(1);
    let radius = gamma * magnitude * (1.0 + 2.0 * gamma + 4.0 * u) + underflow;
    (j, sum, nextafter(radius, f64::INFINITY))
}

The absolute sum rides the same pass as the score, so the enclosure adds no dot products. With radii $r_j$ in hand, the top set $T$ of size $k$ is certified when every kept lower end clears every excluded upper end:

The comparison is strict, and it compares the lowest lower end inside against the highest upper end outside, not rank $k$ against rank $k+1$:

// kernel/epsilon/epsilon/crates/aether-core/src/attention.rs:652-673 @ 36b1400
    let (inside, outside) = ranked.split_at(budget);
    let lowest = inside
        .iter()
        .copied()
        .min_by(|a, b| lower_end(a).total_cmp(&lower_end(b)))
        .expect("budget > 0");
    let highest = outside
        .iter()
        .copied()
        .max_by(|a, b| upper_end(a).total_cmp(&upper_end(b)))
        .expect("budget < len");

    if lower_end(&lowest) > upper_end(&highest) {
        Ok(inside.iter().map(|&(j, _, _)| j).collect())
    } else {
        Err(TopKRefusal::Boundary(BoundaryRefusal {
            inside: lowest.0,
            outside: highest.0,
            gap: lowest.1 - highest.1,
            needed_margin: lowest.2 + highest.2,
        }))
    }

On refusal, certified_or_widened keeps every key whose upper end reaches the lowest selected lower end, at no extra dot products; a NaN or infinite score refuses first and the row falls back to dense. The separation test is ported from separatrix’s error intervals.

The fold score of a loss curve

From the validation losses the kernel keeps the last 64 delay points $p_t = (v_t, v_{t-1}, v_{t-2}) \in \mathbb{R}^3$ and resamples them to uniform arc length. Let $\varepsilon^\ast$ be the largest edge of the resampled cloud’s minimum spanning tree and $m$ the number of resampled points. The loop score is

where $E_\varepsilon$ counts Vietoris–Rips 1-skeleton edges at scale $\varepsilon$ except two-step chords already filled by a triangle, so $c$ upper-bounds Rips $\beta_1$ rather than equalling it. Monotonicity is checked by comparing stored values coordinate by coordinate, with no rounding, so the zero case is exact. The one free constant, $\kappa$, is bounded by a derivation rather than tuned:

The floor comes from a symmetric V. Its descending point $(k, k+1, k+2)s$ and ascending point $(k+2, k+1, k)s$ differ by $(2, 0, -2)s$ for every $k$, so the arms first meet at $\sqrt{8}\,s = \sqrt{8/3}\,\varepsilon^\ast$. The ceiling comes from a monotone stretch: every segment of the delay polyline lies in one closed orthant, so a chord spanning $k$ resampled steps is at least $k\varepsilon^\ast/\sqrt{3}$ long, and since two-step chords are quotiented out, the first chord that can close a cycle spans three steps and needs $\sqrt{3}$. The value 1.68 is the midpoint 1.6825, rounded. The source records the measurement against it: the clean symmetric V scores 0 up to $\kappa = 1.62$ and 0.391 from 1.64. It also records, in the same comment, that the band “is proved for the symmetric V only.” I come back to that under Limitations.

A loop alone does not mean overfitting; a converged run sitting in a noise ball also loops. So the classifier needs a second signal, the drift of the residual $v_t - \text{train}_t$, and it reads underfitting from a third, the participation ratio of the training-loss autocovariances $c_0, c_1, c_2$:

PR is returned as NaN, a refusal, when the training loss varies by less than its own rounding bound, and the Underfit verdict is then withheld. classify decides in a fixed order: non-finite input or an unmeasurable signal gives Collapsing; fewer than 16 samples gives WellFit; training-loss drift of at least 0.50, or a shatter ratio of at least 100 with any rise in training loss, gives Collapsing; $\ell \ge 0.125$ with residual drift of at least 0.05 gives Overfit; a finite PR at or below 0.45 gives Underfit; anything else is WellFit.

The governor, and why T4 is refused

The governor adapts a wake-up threshold $\varepsilon_t$ from an observed deviation $\Delta_t$ with a proportional-derivative step. In code the target rate is $R^\ast = 1000$, $\alpha = 0.01$, $\beta = 0.05$, and $\varepsilon$ is clamped to $[0.001, 10]$:

T4 certifies geometric convergence when the gain margin is below one:

The boot check is a direct evaluation of (9) at the constants every runtime caller passes:

// kernel/seal-os/src/theorems.rs:208-223 @ 36b1400
/// T4/AGCR: `alpha + beta/dt < 1` at the gains and step every runtime
/// governor uses.
fn t4(state: &LiveState) -> Verdict {
    let (alpha, beta, dt) = state.gains;
    let margin = alpha + beta / dt;
    let rho = aether_agcr::contraction_rate(alpha, beta, dt);
    let certified = rho > 0.0
        && rho < 1.0
        && aether_agcr::half_life(rho).is_finite()
        && aether_agcr::gain_margin_stable(alpha, beta, dt);
    let relation = if certified { "<" } else { ">=" };
    verdict(
        certified,
        format!("alpha+beta/dt={:.2} {} 1 at dt={}", margin, relation, dt),
    )
}

Until commit 3c14df0 the same theorem was certified at $\Delta t = 1$. Moving the step to 0.01 is not the whole story, though. Condition (9) treats the map from $\varepsilon$ to $e$ as unit gain; linearising (8) gives $\partial e/\partial\varepsilon = \Delta/\varepsilon^2$, about $10^6$ at the equilibrium $\varepsilon^\ast = 0.001$, and $\alpha K \approx 10^4$ alone exceeds one. No step size satisfies the condition. The repo says what follows: “Earning T4 requires redesigning the governor, not retuning it.”

The Lean files, exactly

The Lean 4 package sits in kernel/aether/aether-verified/lean, on toolchain v4.7.0 with mathlib v4.7.0. Here is what it is, counted at commit 36b1400:

• 11 .lean files, of which lakefile.lean is the build file and four (TestNat.lean, test_nat_chain.lean, test_nat_ineq.lean, test_sub_le.lean) sit outside the lake roots. Two of those use names that no longer exist, so the build does not compile them.
• 28 declarations in the five files the build compiles: EpsilonTheorems.lean 16 theorems and 1 private lemma, Governor.lean 3, Betti.lean 3, Chebyshev.lean 2, Pruning.lean 3.
• sorry appears twice, both inside comments (EpsilonTheorems.lean:7, lakefile.lean:15). In code: 0.
• Four statements conclude True := trivial. They are placeholders and prove nothing: tss_separation_guarantee, gmc_entropy_nonincreasing, phkp_perfect_locality, and upper_bound_sound in Pruning.lean.

The repo’s sentence on scope: “The Lean files prove algebraic side lemmas; no Lean statement is connected to kernel code.” A boot CERTIFIED for T1 or T2 is the Rust kernel evaluating a hypothesis at its runtime parameters, not a Lean proof reaching into the kernel. The statements that matter, verbatim, with what each guarantees:

theorem tss_packing_bound (L : ℕ) (θ_min : ℝ)
    (h_θ_pos : 0 < θ_min)
    (h_θ_lt_pi : θ_min < Real.pi)
    (cap_arg : (L : ℝ) * (Real.sin (θ_min / 2)) ^ 2 ≤ 4) :
    (L : ℝ) ≤ P_max θ_min := by
  unfold P_max
  have hθ2_pos : 0 < θ_min / 2 := by linarith
  have hθ2_lt_pi : θ_min / 2 < Real.pi := by linarith [Real.pi_pos]
  have hsin_pos : 0 < Real.sin (θ_min / 2) :=
    Real.sin_pos_of_pos_of_lt_pi hθ2_pos hθ2_lt_pi
  have hsin_sq_pos : 0 < (Real.sin (θ_min / 2)) ^ 2 := pow_pos hsin_pos 2
  rw [le_div_iff hsin_sq_pos]
  exact cap_arg

This proves that the packing count $L$ is at most $4/\sin^2(\theta_{\min}/2)$, given the cap-area inequality as the hypothesis cap_arg. The geometric fact itself is assumed, not proved; the theorem is the division step.

theorem scm_contraction
    (α_min α_max ε_min ε_max : ℝ)
    (h_α_pos : 0 < α_min)
    (h_α_lt_1 : α_min < 1)
    (h_α_ord : α_min ≤ α_max) :
    telemetry_lipschitz α_min < 1 := by
  unfold telemetry_lipschitz
  linarith

telemetry_lipschitz α_min is defined as 1 - α_min, so this proves $1 - \alpha < 1$ for $\alpha \in (0,1)$. Nothing about any map’s Lipschitz behaviour is proved. The operator the kernel runs, $T(S) = (1-\alpha)S + \alpha S_{\text{pred}}$, appears in the Rust, not here.

theorem agcr_gain_margin_stable (α β dt : ℝ)
    (h_α_pos : 0 < α) (h_β_pos : 0 < β) (h_dt_pos : 0 < dt)
    (h_margin : α + β / dt < 1) :
    0 < governor_contraction_rate α β dt ∧ governor_contraction_rate α β dt < 1 := by
  unfold governor_contraction_rate
  have hβdt_pos : 0 < β / dt := div_pos h_β_pos h_dt_pos
  have hden_pos : 0 < 1 + β / dt := by linarith
  refine ⟨?_, ?_⟩
  · -- 0 < 1 − α/(1 + β/dt)
    -- α < 1 + β/dt is implied by h_margin (α + β/dt < 1 < 1 + β/dt? not quite),
    -- but h_margin gives α < 1 - β/dt < 1 < 1 + β/dt
    have hα_lt : α < 1 + β / dt := by linarith
    have h_frac_lt_1 : α / (1 + β / dt) < 1 := by
      rw [div_lt_one hden_pos]
      exact hα_lt
    linarith
  · -- 1 − α/(1 + β/dt) < 1
    have h_frac_pos : 0 < α / (1 + β / dt) := div_pos h_α_pos hden_pos
    linarith

This is the implication in equation (9): if the margin holds, $\rho$ lies in $(0, 1)$. It is not stated about the update map (8), so it does not say the governor converges, and at the runtime step its hypothesis is false (5.01).

/-- **Scalar Lyapunov descent for a contraction.**

    If `e' = ρ · e` with `|ρ| ≤ 1`, then `V(e') ≤ V(e)`.
    Applies to a map of that form only; the Rust PD step is not one
    (see the module comment). -/
theorem lyapunov_descent (ρ e : ℝ) (h_ρ : |ρ| ≤ 1) :
    V (ρ * e) ≤ V e := by
  unfold V
  have hρsq : ρ ^ 2 ≤ 1 := by
    have := sq_abs ρ
    have hρ2 : |ρ| ^ 2 ≤ (1 : ℝ) ^ 2 :=
      pow_le_pow_left (abs_nonneg ρ) h_ρ 2
    simpa [sq_abs] using hρ2
  have he2 : 0 ≤ e ^ 2 := sq_nonneg _
  calc (ρ * e) ^ 2 = ρ ^ 2 * e ^ 2 := by ring
    _ ≤ 1 * e ^ 2 := by
        exact mul_le_mul_of_nonneg_right hρsq he2
    _ = e ^ 2 := by ring

For a map $e \mapsto \rho e$ with $|\rho| \le 1$, $e^2$ does not increase. The file’s own module comment says “No theorem here is about the Rust governor_step”, and gives the counterexample at $\alpha = 0.01$, $\beta = 0.05$, $\Delta t = 1$, where the refined gain-margin condition holds: from $\varepsilon = 0.28$, $e_{\text{prev}} = 0.5$, $\delta = 0.2$ the step raises $|e|$ from 0.414286 to 0.414650.

theorem chebyshev_one_sided_sq {n : ℕ}
    (x : Fin n → ℝ) (μ : ℝ) (k : ℝ) (h_k : 0 < k)
    (σ_sq : ℝ) (h_σ_pos : 0 < σ_sq)
    (h_σ_def : σ_sq * (n : ℝ) = ∑ i, (x i - μ) ^ 2) :
    (((Finset.univ.filter (fun i => (k * k) * σ_sq ≤ (x i - μ) ^ 2)).card : ℝ))
        * ((k * k) * σ_sq)
      ≤ σ_sq * (n : ℝ) := by
  have h_t_pos : 0 < (k * k) * σ_sq := by positivity
  have base := markov_count_bound (fun i => (x i - μ) ^ 2)
                  (fun i => sq_nonneg _) ((k * k) * σ_sq) h_t_pos
  rw [h_σ_def]
  exact base

The number of points at or beyond $k$ standard deviations, times $k^2\sigma^2$, is at most $n\sigma^2$, which gives the ceiling $n/k^2$ that a memory-pruning rule ported from sigmoid uses. The link to the Rust is only that the Rust checks the inequality this file proves.

/-- TSS Separation: Statement-level placeholder; great-circle distance
    on `S²` requires geometry we do not import here. -/
theorem tss_separation_guarantee
    {P : ℕ}
    (centroids : Fin P → ℝ × ℝ)
    (ε_adaptive : ℝ)
    (h_ε_pos : 0 < ε_adaptive)
    (h_ε_lt_2 : ε_adaptive < 2)
    (h_distinct : ∀ i j, i ≠ j → centroids i ≠ centroids j) :
    -- Statement-level placeholder until S^2 great-circle distance is imported.
    True := trivial

One placeholder, so the shape is visible: it compiles, carries a “0 sorry” chip, and guarantees nothing. The repo’s hygiene gate strips comments, rejects sorry, admit and axiom, and accepts True := trivial only next to a placeholder, skeleton or deferred marker, which is how these four are allowed to stand.

Paging and W^X

Everything above runs in ring 0, so the page tables keep kernel code from being written. memory/virt.rs maps the image from its own PE section table: code is read-execute and never writable, read-only data is non-executable, and kernel data is writable and non-executable. EFER.NXE and CR0.WP are set. A walk splits a 48-bit virtual address into four 9-bit table indices and a 12-bit offset, as translate_in_pml4 does with shifts and masks:

What’s new in it

Each pillar replaces a familiar approach, named here.

Accounting by quantity versus a model of shape. Linux tracks resident pages, CPU time and queue depth per process. Seal OS asks the trainer for two scalars per step and keeps a fixed-size geometric summary of the run, 4,792 bytes per stream, from which it names the regime, without seeing the model.

Patience and gap thresholds versus revisitation. The usual way to notice overfitting is a rule on the validation curve: stop after a number of epochs without improvement (Keras EarlyStopping is the common form), or flag a gap between training and validation loss. stratum asks a different question: whether the validation curve comes back through values it has already visited. That is a property of the curve’s shape in delay coordinates, which a constant offset does not change. The repo’s negative control is a healthy run with exactly such an offset: the gap threshold flags it and stratum does not.

A KV cache in user space versus a prefix tree in kernel memory. vLLM’s PagedAttention manages KV blocks in user space against real models; foliation tests placement and constraint instead: the block table is a path in a tree the kernel owns, each block is a frame from the kernel’s allocator, and eviction is restricted to free faces. The ranking it adds is measured against a null that removes the entrant count: on the boot trace, dropping the entrant count halves the hit rate (952 to 476 bp). The source calls the entrant count “a persistence proxy, and honestly also a frequency counter.”

The ranking is a lexicographic minimum over the free faces:

with $n_\ell$ the entrant count, $d_\ell$ the depth and $u_\ell$ the last-use tick. The locality-only null is $(-d_\ell, u_\ell)$ and LRU is $(u_\ell)$. In code:

// kernel/seal-os/src/ml_engine/foliation.rs:225-233 @ 36b1400
fn rank_of(policy: Policy, l: &Leaf) -> [u64; 3] {
    match policy {
        Policy::Foliation => [l.entrants as u64, u64::MAX - l.depth as u64, l.last_use],
        Policy::Lru => [l.last_use, 0, 0],
        // from https://github.com/triton-lang/kernels/pull/22: sink + local window, as a null
        Policy::Locality => [u64::MAX - l.depth as u64, l.last_use, 0],
        Policy::Random | Policy::Belady | Policy::Adaptive => [0, 0, 0],
    }
}

Comparing floats versus enclosing them. Every discrete answer in the usual numeric pipeline (a component count from a distance threshold, a top-k from sorted scores, a nearest centroid from a dot product) is a bare comparison of computed floats. Seal OS replaces each bare comparison with an enclosure and a refusal. The cost of that change is concrete and the repo records it: the nearest-centroid index’s reported hit rate falls from 1.0000 to 0.9818, because the 91 queries it could not certify go to a full scan instead of being counted as hits.

A theorem banner versus a refusing gate. A system with proofs attached usually prints that they hold. Seal OS evaluates each hypothesis at its running parameters, prints which fail or were never checked, and its CI gate rejects a log that says otherwise.

What no one else built

For each piece I name the closest prior work and say what differs, including where the prior work already does it.

Verified kernels. seL4 has a machine-checked proof of functional correctness of its C implementation in Isabelle/HOL (Klein et al., SOSP 2009). Seal OS has nothing comparable: its Lean files prove algebraic side lemmas and none is connected to kernel code. What Seal OS does instead is evaluate its theorem hypotheses at boot against the live parameters and refuse the ones that fail, including its own convergence claim. That is runtime checking of conditions, not verification, and I would not put it in the same category as seL4’s proof.

Rust research kernels. Theseus (Boos et al., OSDI 2020) restructures OS state into runtime-composable cells in one address space; Redox is a Rust microkernel with drivers in user space; Asterinas is a Rust framekernel that runs Linux binaries with unsafe confined to a small framework. All three are about structure, isolation or ABI, and on those axes Seal OS, a monolithic image with its own 69-call ABI and no ring-3 execution yet, is behind each of them. The difference is elsewhere: where its state lives (points on $S^2$ owned by Voronoi cells) and what it answers about the workload.

Learned and ML-aware OS components. LinnOS (Hao et al., OSDI 2020) runs a small neural network in the kernel to predict, per I/O, whether an SSD will be fast or slow, and revokes a request predicted slow so the application can fail over (paper). LinnOS trains on I/O traces collected from the workload and reports 87 to 97 % inference accuracy. stratum is the opposite construction: it learns nothing. It applies a fixed geometric rule, with a constant derived rather than trained, to two scalars the workload hands it.

Loops in delay embeddings. The idea that a loop in a sliding-window embedding of a time series is a signal is not mine. Perea and Harer’s SW1PerS scores periodicity by the maximum 1-dimensional persistence of a sliding-window point cloud. stratum uses the same family of idea for a different question (did the validation curve revisit its own values?) and in a narrower form: a single scale $\kappa\varepsilon^\ast$ instead of a persistence diagram, a cycle rank that upper-bounds $\beta_1$ instead of computing it, an exact monotonicity certificate for the zero case, and the band $\sqrt{8/3} < \kappa < \sqrt{3}$ derived from the geometry of a symmetric V and a monotone stretch. The derivation of that band, and the use of a fold score as a kernel-side training-regime signal, are the parts I did not find in the prior work I compared against.

Certified β₀. A persistence library such as Ripser computes the barcode and leaves the threshold to the user. Equation (2) says something equivalent in persistence terms: the count at $s$ is certified exactly when the band around $s$ falls in a gap of the 0-dimensional barcode. The mathematics is standard. What differs is the interface: a count is returned only with that gap as its certificate, and otherwise a refusal names the tree edge in the band, with a scale-safe distance so the heights themselves do not overflow.

Error-bounded filters. The closest prior work to certify-or-refuse is Shewchuk’s adaptive-precision geometric predicates (1996/1997), and the filtered predicates in computational-geometry libraries that follow them. A predicate evaluates in floating point with an error bound; if the bound cannot certify the sign, it escalates precision until it can. Seal OS uses the same filter idea with Higham’s bound on three discrete answers (a component count at a scale, an attention top-k set, a nearest centroid on $S^2$), and on failure it does not escalate. It refuses, widens the row, or scans every centroid, and the refusal names the input. The filter is Shewchuk’s idea; the refusal as a returned value across a kernel interface is the difference.

Prefix caching. Here the prior work already does most of it. SGLang’s RadixAttention keeps the KV cache in a radix tree and evicts least-recently-used leaves first, recursively, while protecting nodes the running batch uses. That is free-face eviction under LRU. vLLM’s automatic prefix caching hashes each block together with the tokens of its prefix, evicts unreferenced blocks by LRU, and on a tie evicts the block at the end of the longest prefix first, which is a depth term. So the connected-subtree constraint is not new, and the syscall-facing cache in Seal OS, which defaults to LRU, is the RadixAttention policy run in kernel memory. What differs: the tree, its frames and its eviction live in the kernel and draw on the kernel’s own allocator; a child is shared only on an exact token match even though the key is a 64-bit digest; and the entrant-count ranking is tested against a null, Belady’s oracle and 32 random seeds on a trace where it wins and one where it loses, with both outcomes published. Whether any of this beats user-space placement has not been measured.

What survives the comparisons. The mechanism I did not find elsewhere is the combination: one certify-or-refuse rule applied across component counts, attention top-k, nearest-centroid lookup on $S^2$, the zero case and the trend signal of a fold score with a derived scale band, and the kernel’s own boot theorems, with the theorem refusal enforced in CI. It is not applied everywhere: a window that turns is scored from its Rips complex without a certificate, and ManifoldFS places files with an index that carries none. Each part has a named ancestor above; the combination, and the kernel refusing its own convergence theorem at the step it runs, are what I add.

Limitations

These are stated as the repo states them, and where the code at 36b1400 has moved past a document, I say which.

No user mode. No instruction has executed in ring 3. /bin/init is absent and the kernel falls back to its in-kernel desktop; with a /bin/init present, boot stops after loading it. The repo’s record, made at 9ebbe2e, says syscall_entry ran on the user’s stack with no swapgs. At 36b1400 it executes swapgs and loads the task’s kernel stack; since nothing has run in ring 3, that path has not been exercised from user mode. The record also says no task is ever scheduled; at this commit the scheduler adopts the boot thread in init, and I have not run it, so I make no claim either way. Application-processor bring-up exists and is not called.

No real models. Every stratum and foliation number comes from a synthetic fixture. The README: “It has never seen a real model, and its verdict is advisory: nothing enforces it yet.” On the chat trace foliation loses to LRU (5,284 against 8,068 bp), to the locality-only null (6,818) and to all 32 random seeds; with 16 live conversations it reverses again in one mutation build. The reported results are at one pool size (24 blocks); the source also replays each trace at six sizes from 8 to 48 blocks, which the repo’s one-pool-size limit does not mention. Whether kernel placement of the KV cache buys anything over user-space PagedAttention has not been measured.

The κ band covers one shape. The band in (6) is proved for a symmetric V only. A V descending at 0.005 and climbing at 0.01 per step scores 0.016 at $\kappa = 1.72$ and 0.406 only at 1.8, above the ceiling, so no choice of $\kappa$ inside the band detects it.

T4 is refused and needs a redesign. No step size earns it, because the loop’s gain is about $10^6$ and (9) assumes one. System calls 100 and 102 still print FAILED for every theorem that is not certified, eight of the ten, where the boot log, the ManifoldFS status and the theorem viewer print CERTIFIED, NOT CERTIFIED or NOT CHECKED. Seven of the ten boot lines are not checked.

Lean is not connected to kernel code. Eleven .lean files, 0 sorry in code, four True := trivial placeholders, and the proved statements are algebraic side lemmas. None is linked to the Rust by refinement.

CI is red. The QEMU job of run 36165748105 fails at the language-hygiene gate, on scripts/ci_parity.sh, and the gates after it in that job did not run. The kernel’s own unit tests are not run by CI: the crate is outside the Cargo workspace, and the Kernel Tests workflow last executed on 2026-08-11 (514 of 514). Two of the 25 boot milestones are string matches that prove little.

One machine, no comparison. Hardware is one QEMU configuration (q35, OVMF, AHCI, 4 GiB, no NIC). The GPU path ran only on its CPU fallback. Every cycle count is QEMU TCG with an emulated TSC. No comparison against Linux or Ubuntu has been run. Nothing here is production-tested.

Security is measured, not complete. W^X holds since b3cf934, but the probe classifies per mapping; SMEP and SMAP were not exercised because the CI CPU model lacks them; KASLR randomises mappings, not the image base. manifold_acl::check_access denies access Linux permits: a uid-1000 process cannot read a 0644 root-owned file. ManifoldFS places files with its own cell index, fs/voronoi_cap.rs, which carries no certificate. No ext4; TLS accepts Ed25519 certificates only; no socket system call exposes the network stack.

The docs lag the code. The drift I found at 36b1400:

• README and THEOREMS.md quote 9 of 10 theorems VERIFIED; ... T1-T3, T5 ACTIVE; the code prints 2 certified, 1 not certified (T4), 7 not checked, and T3 and T5 are not checked.
• THEOREMS.md cites line ranges for init_theorems and a verify_topology_theorems symbol that is no longer in kernel/seal-os/src, and its scheduler and ManifoldFS line references point elsewhere at HEAD.
• RESULTS.md’s syscall-entry limit predates the swapgs entry now in userspace.rs.
• RESULTS.md says FitAction is “enforced nowhere”; at HEAD a threshold is published that only an unconstructed preset reads, so the effect is the same.
• The older papers under docs/research/ claim a 241 to 1500× KV-cache speedup over LRU and a 21.8M-token horizon. Neither figure appears in README, RESULTS or THEOREMS, and neither is a current result. The current foliation numbers are the ones above.
• RESULTS.md’s subsystem table sums to 92,037 of the 96,110 kernel lines it states (at 9ebbe2e); 4,073 lines are not itemised.

Read more

The project page at teerth.dev/Epsilon-Hollow draws the results live. The source is github.com/teerthsharma/Epsilon-Hollow, and the short link is teerth.dev/epsilon-hollow. Key files at commit 36b1400:

• README.md: the idea and the four pillars.
• docs/RESULTS.md: every number with its provenance, equations (1) to (9), the Limits list.
• kernel/seal-os/src/theorems.rs: the boot theorem lines.
• kernel/aether/aether-verified/lean/: the Lean 4 package.
• certified_betti.rs, attention.rs, trajectory_shape.rs and foliation.rs: the certified kernels and the KV prefix tree.

Related essays on this site: separatrix, which grew out of this work, and Aether-Lang, whose no_std runtime the kernel embeds. The upstream fixes above are at openxla/xla#46539 (closed, and landed on main through Google’s internal import as 3d5df1d) and tensorflow/tensorflow#124410 (merged; short link teerth.dev/tensorflow-124410).

@misc{sharma2026epsilon-hollow,
  author = {Teerth Sharma},
  title = {Epsilon-Hollow},
  howpublished = {\url{https://teerth.blog/epsilon-hollow}},
  year = {2026},
  note = {CC BY 4.0}
}