Proving Away the Retry Ceremony: Domain Algebra and Terminal Precedence

AnankeLabs builds KAIROS, a deterministic runtime safety substrate that evaluates autonomous agent actions across robotics, cybersecurity, and AI systems before execution commits. Turning the KAIROS Rust evaluation kernel from an exploratory simulation prototype into a hardened, deterministic safety runtime consumed most of September and October 2026 and added no product features. Instead, the work was structural: interrogating every state transition, fallback branch, floating-point intrinsic, and cache lookup until each mechanism was either proven necessary and sound or excised from the codebase.

Every defect examined across this series was identified and resolved internally before any KAIROS release was distributed outside the company, with the fixes shipping in the next tagged release.

Following our release provenance overhaul, we are documenting three of those engineering campaigns as the Kernel Hardening Triptych:

Installment	Kernel Subsystem	Core Invariant Established
Part I (this article)	Causal Resolver & Session Ingress	Enforced stability domain ($\lambda, \gamma \in [0, 1]$), a tick-local decree overlay, and paradox rejection that no earlier override can undo
Part II	Procedural Topology Generator	Bit-identical topology hashing (sin(angle)) across native x86_64 and aarch64, WebAssembly, and a TypeScript reference verifier
Part III	Reachability Kernel & Frame Cache	Every reused reachability frame equals a fresh solve, with the verification cost measured on non-turbo silicon

This opening installment examines how enforcing a bounded input domain at ingress allowed a mathematical proof to replace a stateful replay-and-rollback ceremony, and how tearing out that ceremony exposed a subtle precedence flaw at the boundary between causal rejection and human-in-the-loop operator overrides.

What the Legacy Resolver Actually Did

Inside the KAIROS evaluation kernel, time advances in discrete steps called ticks, and agents move across a discrete lattice of nodes. When two or more agents land on the same node during a tick, they form a collision component. On each tick, the causal resolver checks every colliding pair of agents within a component to see whether their interaction drops below a critical stability floor, a condition the specification calls a causal paradox (a pairwise stability violation on a shared node, rather than a logical contradiction in the policy rules).

For any colliding pair of agents $a$ and $b$, stability is defined as

$$S = \frac{\gamma_a + \gamma_b}{\lambda_a + \lambda_b + \varepsilon}, \qquad \varepsilon = 10^{-6},$$

where $\lambda$ represents an agent’s agency (its drive to explore) and $\gamma$ represents its commitment (its caution or aversion to risk). The ratio compares the pair’s combined caution against their combined agency, while $\varepsilon = 10^{-6}$ guards against division by zero when $\lambda_a = \lambda_b = 0$ (since $\lambda = 0$ is a valid parameter value). A colliding pair is classified as a paradox whenever $S < 0.15$; exact equality ($S = 0.15$) counts as stable.

Carried over from our early TypeScript prototype, the legacy resolver responded to the first unstable colliding pair by executing a four-step retry ceremony:

1. Restore a snapshot of the agent states and the random number generator captured at the start of the tick.
2. Apply a decree (a temporary $\gamma$ boost intended to stabilize an unstable collision) by raising $\gamma$ by $0.2$, capped at $1.0$, for the two agents in that pair.
3. Replay the exact same candidate moves and check whether the pair still occupied the same node.
4. If the pair still shared the node, restore the snapshot a second time and force every agent in the simulation to stay in place for the tick.

The flaw sat right in the evaluation criterion of the third step. The decree raised $\gamma$, yet the retry replayed identical moves and judged success by position rather than stability. Because a pair that collided once collided on the same node again under identical moves, the fourth step ran on every unstable collision, including those with completely valid parameters. What looked in the source like a four-stage defensive hierarchy behaved in practice as a blunt rule: any paradox froze every agent for the tick.

The legacy design also restored the snapshot taken before agent activation and other start-of-tick lifecycle routines, so a retry could quietly undo work the tick had legitimately performed.

Making the Domain an Invariant

Eliminating the retry loop began with locking down the inputs. Although the specification had always defined $\lambda$ and $\gamma$ on the unit interval $[0, 1]$, the v1.0 engine never enforced that bound at runtime: a setter call or an event script could hand the resolver any float. In September (e7ca043), we made $\lambda, \gamma \in [0, 1]$ an enforced invariant across every ingress surface. Engine configuration, policy setters, and event loading (load_event_script, schedule_event) now reject NaN, infinities, and out-of-range values through validate_policy_overrides and validate_enforced_limits before any state changes occur. Because deserialized payloads pass through those same engine methods, the validation holds regardless of transport.

With $\lambda, \gamma \in [0, 1]$ enforced, the decree’s stabilizing effect follows in five steps directly from the specification:

1. Initial instability bound. For any colliding pair $(a, b)$ that is unstable before the decree, $S < 0.15$. Because $\lambda_a, \lambda_b \in [0, 1]$, the denominator satisfies $\lambda_a + \lambda_b + \varepsilon \le 2 + 10^{-6}$, which forces the numerator below the product: $\gamma_a + \gamma_b < 0.15 \times (2 + 10^{-6}) = 0.30000015$
2. No clamping on unstable pairs. Because $\gamma_a, \gamma_b \ge 0$ and their sum is below $0.30000015$, each satisfies $\gamma < 0.30000015 < 0.8 = 1.0 - 0.2$. So $\gamma + 0.2 < 1.0$, the cap never binds, and both agents receive the full $+0.2$.
3. Post-decree numerator floor. After the $+0.2$ overlay is applied to each member of the unstable pair, their combined commitment is at least $\gamma'_a + \gamma'_b = \gamma_a + \gamma_b + 0.4 \ge 0 + 0.4 = 0.4$.
4. Worst-case post-decree stability. Dividing that minimum post-decree numerator by the maximum possible denominator yields a strict lower bound across all valid inputs: $S_{\text{decreed}} \;\ge\; \frac{0.4}{2 + 10^{-6}} \;\approx\; 0.1999999 \;>\; 0.15$
5. Already-stable pairs in the same component. Steps 1 through 4 cover every pair that was unstable before the decree. The remaining case is pairs in the same component that were already stable ($S \ge 0.15$) before the decree. Because the decree only increases $\gamma$ (clamped at $1.0$) and leaves $\lambda$ untouched, the stability ratio $S$ for any already-stable pair in that component can only increase or stay the same, so it remains stable as well.

Accounting for the $\varepsilon = 10^{-6}$ term in the denominator places the exact lower bound at $0.1999999$ rather than a rounded $0.20$, a distinction our internal review insisted on keeping. Because a decree always restores stability on valid inputs, there is nothing left for a runtime retry loop to test.

One Physical Application, Two Read-Only Assessments

That proof allowed us to delete the replay branch rather than keep it around as dead code:

• Geometry applied once. The engine applies candidate moves a single time and assesses stability under the agents’ stored parameters.
• A tick-local decree overlay. Whenever any collision component contains an unstable pair, the resolver collects the affected agent IDs into a single per-tick set and runs a second read-only assessment under an overlay that adds $+0.2$ (capped at $1.0$) to $\gamma$ for each agent in that set. Because an agent occupies a single node at any given tick, it belongs to at most one collision component, while collecting agent IDs into a set prevents an agent involved in multiple unstable pairs on that same node from receiving stacked $+0.2$ boosts. Each affected agent gets exactly one overlay value (which is all the five-step proof requires), and the overlay is never written back to stored AgentPolicy state, so it cannot leak into later ticks.
• A typed error for the impossible case. If the post-decree assessment ever reported instability, the engine would restore the agents and the random number generator from a physics snapshot and return a typed PostDecreeInstability error. While this branch is unreachable under the proven invariant, we retain it as a fail-closed guard against future changes to a constant or the input domain, or runtime state corruption.
• Atomic rejection at ingress. A rejected ingress payload leaves the parent engine state, the Mulberry32 random number sequence, and the reachability caches untouched, and commits no trace step.

One boundary gap in intra-tick atomicity remains open and is tracked separately (AUD-006). When a candidate transition fails mid-tick, the physics snapshot restores agent states and the random number generator. But if an event fails partway through a tick’s scheduled batch, the events applied before it stay applied, the rest of the drained batch is lost, and the tick does not advance. Start-of-tick lifecycle effects are not rolled back either.

Locking the Invariant Against Regression

To ensure future edits or language bindings cannot smuggle unvalidated floats back into the solver, we locked the domain invariant down at three levels:

1. A crate-private PolicyValues type. In crates/kairos-engine-core/src/policy_domain.rs, validated stability parameters live inside a struct with private fields that code outside the engine crate cannot construct directly.
2. Negative tests in every binding. Dedicated tests across the Rust core, the C FFI (kairos_last_error), the Python bindings, and WebAssembly each inject NaN, infinite, and out-of-range policy values. The Rust test compares private subsystem state (loss, reachability, and special nodes) before and after the rejected call, while the C, Python, and WebAssembly tests verify every public state accessor.
3. A golden paradox corpus. Twelve committed trace and prophecy files (six scenario pairs totaling 25,329 bytes under tests/fixtures/rust-golden/paradox/cases) are regenerated and compared byte for byte in CI. During review, four deliberate corruptions (a changed digit, a missing file, an extra file, and an emptied evidence vector) were each caught.

Closing the Override Precedence Gap

Reworking the resolver also exposed a safety-relevant ordering flaw between causal rejection and human-in-the-loop operator overrides. In KAIROS, the session gateway sits in front of the core engine as the enforcing policy boundary that decides whether a proposed action may be committed in a live system. While building a new signed-token regression test, we found that a valid signed override issued by an authorized operator for an earlier rejection in an evaluation (turning a state rejection into a pass) survived a paradox classified later in that same evaluation. This was not an unauthenticated exploit, since it required a genuine signed token from an authorized operator, but in an enforcing gateway mode it meant an override intended for a different rejection could allow an action carrying paradox evidence to be admitted.

Commit c5deac4 closed the gap so that paradox classification now takes terminal precedence over any previously applied override. When a pairwise collision violates the stability floor, an operator token issued for an earlier check in the pipeline cannot turn that evaluation back into a pass.

The core engine and the session gateway divide responsibilities as follows (where a prophecy is the engine’s structured audit record of an unstable colliding pair):

Layer	Outcome	Effect
Engine	No paradox	Candidate state commits; stored AgentPolicy unchanged
Engine	Admitted by decree	Candidate commits under the tick-local overlay; one Prophecy per unstable pair is recorded with unresolved = false; stored AgentPolicy unchanged
Engine	Typed invariant error	Unreachable on valid inputs; agents and RNG restored, error returned
Gateway, enforcing modes (StateGate, StatePlusActionGate)	RejectParadox	Any initial paradox evidence rejects the action, even one the engine can admit by decree; no earlier override can turn it into a pass
Gateway, Observe mode	Pass with reason DualAdministratorParadox	The hazard-gate detail and prophecies are returned in the evaluation response for offline audit

In the Observe row, DualAdministratorParadox is the gateway’s reason code for paradox evidence (two independent controllers claiming the same node in the same tick) and is used across every domain. That split between the two layers matches the role of each: the engine admits the co-occupancy for that tick only, so the simulation can continue; if the agents are still together next tick, a fresh paradox assessment runs. The enforcing gateway, by contrast, refuses to let a real action through if it needed a decree to stabilize.

Bounding Multi-Actor Ingress at 64 Agents

A deterministic runtime must also bound the work an untrusted or external request can trigger. Inside the resolver, pairwise collision analysis scales quadratically for agents sharing a node, and the resulting paradox evidence log grows without an internal cap. While the core engine permits arbitrary agent counts for trusted local callers, our cloud simulation service (kairos-nexus) previously passed caller-supplied agent arrays directly into WebAssembly engine allocation (resetAgents inside applyAgentSetups) without an upper bound. Two controls now run before engine allocation, database persistence, or any response headers are streamed:

1. A 64-actor ceiling (MAX_SIMULATION_AGENTS = 64). On the domain path, the raw entity count is checked before adapter encoding and the encoded agent count after it; applyAgentSetups then rechecks the 1..=64 bound across inline creation, domain creation, and database rehydration alike. The ceiling admits our eight-agent reference example and our 64-agent (2,016-pair) evidence characterization case. It is an operator capacity policy to bound multi-agent evaluation work rather than an empirically measured memory or latency cliff.
2. A default-deny principal allowlist. Requests supplying custom multi-actor collections are gated by a PostgreSQL table in which each row names a single principal, either an authenticated user_id or an api_key_id. Allowlisting a user for interactive testing therefore never authorizes the API keys that user owns. An empty table denies custom multi-actor collections to everyone, which is how it shipped to production.

Aligning Public Claims With Verified Code

In the final phase of the campaign, we audited 102 public and internal surfaces (our bridge library, schema, this website, and supporting records) against the post-reform source. Fifty-one were already accurate, 21 were updated to match the code, and 25 historical records were kept and labelled as historical. The remaining five were public determinism statements we could not yet verify. We held them unchanged, each tagged in the audit ledger with the open finding it depended on and the condition for revisiting it. Engine documentation was corrected separately.

That audit is also what caught our public compliance copy outrunning our verification evidence. Our explainers on the EU Machinery Regulation and Technical File construction stated identical verdicts on any execution hardware, at a time when our own invariant scorecard listed bit-for-bit determinism as insufficiently tested. We qualified both explainers immediately and opened the engineering work to close the gap.

One root cause lay in procedural topology generation, which hashes salted (t, b, seed) coordinates through f64::sin(angle). Standard math libraries in glibc, Rust’s WebAssembly target, and JavaScript engines do not all agree on the last bit of a sine. How we measured that disagreement across 141 million tuples, and brought native, WebAssembly, and TypeScript to bit-identical topology on a qualified corpus, is the subject of Part II: One Sine Wave, Four Runtimes.