AETHER Runtime Integration
Can an autonomous agent have mathematically-proven resource safety?
Autonomous AI agents manage memory, network connections, compute sessions, and money without human oversight. Most runtimes use ad-hoc limits and hope-based garbage collection. The question is whether we can replace hope with proof.
Teerth Sharma's AETHER paper defined four mathematical primitives for LLM inference: Cauchy-Schwarz block pruning, PD governors with Lyapunov stability, Chebyshev GC guards, and Betti approximation bounds. We formalized all four in Lean 4 and published the proofs on our Paper → Proof → Code pipeline.
This project is the next step: taking those verified artifacts and integrating them into AgentHALO, our autonomous agent runtime, as the actual resource control layer. The governor equations running in production are the same equations the Lean kernel checked. Every status field, every dashboard indicator, every API response derives its regime label from the real governor state—not a hardcoded string. And where the formal proof ends and engineering begins, the system says so honestly.
Why this is Ruliology
Teerth's paper defined the primitives. Our Lean formalization proved them. But the ruliology—the discovery that emerges when you pull a thread through the verification loom—is what happened next.
Formalizing the PD governor forced us to confront what multi-step convergence actually means. The Lean proof establishes single-step Lyapunov descent from rest. Multi-step convergence is not proved, and we found a counterexample showing it cannot be, under the given conditions. This distinction—invisible in the original paper—became the design principle for the production system: governors track their own regime honestly, and quiescent reset periodically returns them to the formally-verified starting state.
Formalizing the Chebyshev guard revealed that coupling decay to operation count (the natural engineering choice) destroys the statistical discrimination the inequality guarantees. Wall-clock decay preserves it. This fix would not have been obvious without the formalization forcing us to trace exactly what the inequality requires.
The formal-empirical boundary itself is a ruliology discovery: when you label every function as either “verified core” or “engineering wrapper,” the architecture self-organizes into thin verified shells around stateful engineering layers. The pattern is reusable beyond this project.
Lean 4 (HeytingLean/Bridge/Sharma/)
AetherGovernor.lean ─── lyapunov_descent, validatorRegime
AetherChebyshev.lean ── chebyshev_finite, gc_25_percent_bound
AetherBetti.lean ────── betti_error_bound, heuristic_sound
AetherPruning.lean ──── prune_safe, can_prune_sound
│
CAB Pipeline (Lean → C → Rust)
│
Safe Rust (nucleusdb/src/halo/)
governor.rs ────────── GovernorState, step(), regime_label()
governor_registry.rs ─ GovernorRegistry, observe(), soft_reset()
governor_telemetry.rs shared EWMA, quiescent reset
chebyshev_evictor.rs ─ ChebyshevEvictor, eviction_candidates()
topo_signature.rs ──── fingerprint(), compare()
│
Production Wiring (nucleusdb/src/)
proxy.rs ──── ProxyGovernorRuntime (gov-proxy, gov-cost)
blob_store.rs ─ BlobStore eviction (gov-memory)
vector_index.rs VectorIndex eviction (gov-memory)
pty_manager.rs ─ PtyManager (gov-compute, gov-pty)
ws_bridge.rs ─── WebSocket comms (gov-comms)
│
Dashboard & CLI
api.rs ──── /governor/status, /governor/proxy/status
mod.rs ──── background quiescent reset (10s interval)
app.js ──── governor sparklines, status badges
agenthalo ─ `governor validate` subcommandWhat is proved vs. what is engineering
FORMALLY VERIFIED (Lean 4)
- • Single-step Lyapunov descent from rest, no-clamp
- • Gain condition: α + β/dt < 1 with dt ≥ 1
- • Chebyshev guard: ≤ n/k² reclaimable items
- • Uniform decay preserves guard status
- • Betti error bound: β̂&sub1; ≤ b + (n − 3)
- • Pruning safety: zero false negatives
ENGINEERING (labeled honestly)
- • Multi-step governor convergence (NOT proved)
- • Stateful ChebyshevEvictor liveness tracking
- • Wall-clock decay coupling
- • Quiescent reset timing (30s window)
- • ProxyGovernorRuntime backpressure policy
- • Gov-memory aggregate (synthetic dashboard metric)
PD Governor & Lyapunov Stability
Proportional-derivative controller with machine-checked Lyapunov descent. Gain condition α + β/dt < 1 from Lean validatorRegime. Governor registry with per-instance telemetry, oscillation detection, and quiescent reset to re-enter formal regime.
Key Results
- •lyapunov_descent (single-step energy non-increase)
- •govError_contraction_noclamp (error contraction)
- •validatorRegime (gain condition: α + β/dt < 1, dt ≥ 1)
- •Regime tracking: from-rest → engineering multi-step → quiescent reset
- •5 governor instances: proxy, comms, compute, cost, PTY
Chebyshev Eviction & Liveness Guards
Finite-sample Chebyshev inequality for garbage collection safety. Guard guarantee: items within k standard deviations of mean liveness are never evicted. At most n/k² items are reclaimable. Wall-clock decay, least-live fallback, quiescent governor reset.
Key Results
- •chebyshev_finite (≤ n/k² reclaimable items)
- •gc_25_percent_bound (at most 25% false collections at k=2)
- •uniform_decay_preserves_guard (scaling invariance)
- •Wall-clock decay via powf (decoupled from operation throughput)
- •Least-live fallback when Chebyshev set is insufficient
Betti Topological Fingerprinting
Binary structural integrity via topological fingerprints. 4-window heuristic Betti approximation with formal error bound. Positioned as secondary deploy preflight signal alongside SHA-256 as primary authenticator. Flags unexpected structural drift beyond the proven bound.
Key Results
- •betti_error_bound (β̂₁ ≤ b + (n − 3))
- •heuristic_window_bound (β̂₁ ≤ n − 3)
- •SHA-256 primary + Betti secondary deploy preflight
- •Topology record persistence with content-addressed keys
Production Integration & Hostile Audit
Engineering wiring of verified primitives into AgentHALO production paths. ProxyGovernorRuntime with RAII permits and CAS backpressure. Shared comms telemetry (eliminating double-counting). Dashboard API surfaces with honest regime labeling. Background quiescent reset for all 5 governor classes. Two hostile audit rounds, all findings addressed.
Key Results
- •ProxyGovernorRuntime: CAS-loop backpressure with RAII ProxyPermit
- •Shared EWMA telemetry (single OnceLock, no duplicate state)
- •All regime labels derived from actual state (not hardcoded)
- •710 tests pass, 0 fail, 0 sorry
- •2 hostile audits: 5 bugs found and fixed, 3 design concerns closed
Hostile Audit Results
Found 5 bugs (2 medium, 3 low) and 3 design concerns:
- • Bug 1-2: gov-memory synthetic snapshot hardcoded false regime/gamma/stability
- • Bug 3: evictor decay coupled to operation count, not wall-clock time
- • Bug 4: duplicate EWMA state in ws_bridge and didcomm_handler
- • Bug 5: blob_store eviction logic had zero test coverage
- • DC1: storage governors permanently exited formal regime
- • DC2: gain_margin_refined was dead code
- • DC3: soft_reset was never called in production
All 5 bugs fixed, all 3 design concerns closed. No regressions.
- • gov-memory now derives all fields from actual governor state
- • Decay uses wall-clock seconds via powf (decoupled from throughput)
- • Single shared EWMA via OnceLock in governor_telemetry.rs
- • 5 new blob_store tests (guard, fallback, stats, decay, quiescent reset)
- • All governors have quiescent reset paths (30s idle / 0 sessions)
- • Dead code removed, soft_reset wired to production maintenance loop
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is a cryptographically anchored MCR documenting authorship, contribution level, and provenance chain. Artifacts are content-addressed and pinned to IPFS.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
AETHER Runtime Primitives for LLM Inference
Contributor
Teerth Sharma
Independent Researcher
Original mathematical theory defining four runtime primitives for efficient LLM inference: Cauchy-Schwarz block pruning for zero-false-negative attention sparsification, proportional-derivative governors with Lyapunov stability guarantees, Chebyshev inequality guards for garbage collection safety, and Betti number approximation bounds for topological binary authentication. This seed contribution provided the mathematical foundations that all subsequent formalization, verification, and production integration builds upon.
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Lean 4 Formalization of AETHER Primitives
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 implementation of all four AETHER mathematical cores. 4 proof modules plus 4 sanity-test modules, 23 sorry-free theorems, 818 lines of proof code. Built on Mathlib and HeytingLean chain complex infrastructure. Kernel-verified by the Lean 4 type checker with zero sorry/admit gaps.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
AETHER Verified Kernel — 6-Round Hostile Audit
Contributor
Apoth3osis Labs
R&D Division
Complete formal verification of the AETHER Lean 4 formalization through six rounds of adversarial hostile audit. R1: 6H/4M/3L findings. R2: 0H/3M/1L. R3: CLEAN. R4: 0H/1M/0L. R5: CLEAN. R6: CLEAN. All findings resolved. Final two consecutive rounds CLEAN. Verified C and safe Rust artifacts generated via CAB pipeline with certificate hashes at each transformation step. All artifacts content-addressed and pinned to IPFS.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
AETHER Production Integration into AgentHALO
Contributor
Apoth3osis Labs
R&D Division
Bridge connecting formal proofs to production runtime. Verified Rust primitives integrated as the actual resource control layer in AgentHALO: 5 governor instances (proxy, comms, compute, cost, PTY), Chebyshev eviction for blob/vector stores, Betti topological fingerprinting for deploy preflight. 710 tests, 0 failures, 0 sorry. Every regime label derived from actual governor state. Formal-empirical boundary explicitly labeled throughout. Two production hostile audits: 5 bugs found and fixed, 3 design concerns closed.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026