Correctness by Construction

Three different communities, separated by decades and disciplines, arrived at the same conclusion.

Joe Armstrong building Erlang at Ericsson in the 1980s concluded that fault tolerance cannot come from defensive coding within a process. The process that detects an error crashes cleanly. Its supervisor restarts it. State recovers from durable storage. The architecture is what makes the system reliable — not the programmer’s discipline inside any individual component.

Jane Street spending years on the Oxidizing OCaml series concluded that data race freedom, memory safety, and ownership semantics should be type-level properties. The compiler enforces them. Programmers do not have to remember to enforce them, because remembering is not a reliable mechanism at scale.

Gerard Holzmann at NASA JPL concluded that safety-critical code needs properties that can be proved, not just tested. Testing demonstrates the presence of correct behavior on tested paths. Proof demonstrates the absence of incorrect behavior on all paths. For spacecraft software, where a single bug can end a billion-dollar mission and no human can intervene to fix it, only proof is sufficient.

The thesis they share: correctness is a property you design in, not a quality level you test toward. The system architecture makes entire classes of failure structurally impossible. Not unlikely. Impossible.

ClawQL Streams — and the cellrt / TEE path that hosts it — is where this thesis becomes concrete for agentic infrastructure. This pairs with the Effect-TS migration (typed errors and Layer DI on the TypeScript side) and the Hardened Agentic Stack.

What each tradition contributes

Armstrong: supervision trees and isolation

Armstrong’s central insight is that isolation plus supervision — not defensive coding — produces reliable systems. A process that encounters an unexpected state should not try to recover from inside that state. It should crash. The supervisor watching it restarts it into a known good state. State that must survive restarts lives in durable storage, not process memory.

For cellrt / TEE, the cell lifecycle follows this model. A cell that encounters an unrecoverable error during tool execution does not attempt heroic recovery. It terminates, expires its virtual key via the Drop trait, flushes its audit trail, and releases its coordination lease. The fleet coordinator detects the expired lease and another node resumes from the LTX segments in the bucket. Restart strategies are declared on the supervision tree — which components restart always, which restart only on abnormal exit, which never restart — rather than scattered through ad hoc error handlers.

Armstrong also formalized what gen_statem makes explicit: State(S) × Event(E) → Actions(A), State(S'). State enter callbacks fire on every transition into a new state, co-located with the transition logic, guaranteed to run regardless of which event triggered the transition. For an Agent cell that means the cleanup on the way into Terminating runs whether the cell finished normally, hit a budget cap, or hit a Vault error. Cleanup is declared once, at the state boundary.

Jane Street: types as correctness certificates

The Oxidizing OCaml series — Locality, Rust-Style Ownership, Data Race Freedom — documents Jane Street’s multi-year effort to bring Rust’s correctness guarantees into OCaml without giving up garbage collection. OxCaml adds modes to OCaml’s type system: locality, uniqueness, linearity. Same properties Rust’s ownership system provides, formalized as a type-level discipline.

Uniqueness is the right model for the virtual key lifecycle. A unique value — in OxCaml’s terms, or a non-Clone, non-Copy type in Rust — can exist in exactly one place at a time. When it moves, the original is gone. When it drops, cleanup runs:

// VirtualKey is not Clone, not Copy
// It can only exist in one cell at a time
// Drop expires the key regardless of how the cell exits
pub struct VirtualKey {
    id: Uuid,
    cell_id: CellId,
    budget_tokens: u32,
    tokens_used: Arc<AtomicU32>,
    expires_at: DateTime<Utc>,
    state: Arc<RwLock<VirtualKeyState>>,
}

impl Drop for VirtualKey {
    fn drop(&mut self) {
        // Key expiry runs regardless of exit path —
        // panic, timeout, budget exhaustion, normal completion
        tokio::spawn(self.expire_async());
    }
}

The process-level uniqueness invariant — no two cells hold the same active key — is enforced by the type system. You cannot clone a VirtualKey. You cannot copy it. The compiler refuses.

Jane Street’s data race freedom work maps onto Rust’s Send and Sync bounds. A cell’s SQLite connection is not Send. It belongs to exactly one Tokio task. Tokio’s spawn requires Send. Share the connection across tasks by accident and the compiler refuses before the code ever runs.

NASA / Ada / SPARK: what types cannot prove

The Power of 10 rules and the Ada/SPARK tradition add the layer type systems cannot reach. Bounded loops. Minimum assertion density. No dynamic allocation after initialization. All warnings as errors. SPARK goes further: GNATprove verifies preconditions, postconditions, data invariants, and information-flow isolation — not sampled. Proved for all inputs.

(The “cleanest large-scale software” story people sometimes misremember as ColdFusion is the shuttle primary avionics software at IBM Federal Systems — roughly 0.01 defects per 1,000 lines, driven by specification-before-code, independent review layers, and defect-as-process-driver. SPARK Ada is the formally verifiable lineage that carries the same instinct into military and aerospace control software.)

The gap for Streams / cellrt is between “the type system prevents bad state transitions at the call site” and “every cell that enters Spawning eventually reaches Dead.” The first is a safety property — Rust’s exhaustive enum matching enforces it. The second is a liveness property — no mainstream type system proves it. A cell could wait for Vault indefinitely. The type system has no opinion.

Fleet-wide virtual key uniqueness — not just within a process, but across all nodes under concurrent spawns — is a global property. Rust prevents data races within a process. It does not prove that two nodes could not independently issue the same key ID if distributed coordination is wrong.

Those are the properties TLA+ addresses. Written before the Rust code, not after:

(* No two cells in Running state share a virtual key *)
KeyUniqueness ==
  \A c1, c2 \in RunningCells :
    c1 # c2 => cells[c1].virtualKeyId # cells[c2].virtualKeyId

(* Every spawned cell eventually reaches Dead *)
CellLiveness ==
  \A c \in SpawnedCells : <>(cells[c].state = "Dead")

(* WORM entries are never modified after writing *)
WORMAppendOnly ==
  [](\A seq \in 1..Len(wormLog) :
    [](wormLog[seq] = wormLog[seq]))

TLC runs these over the reachable state space. Pass → the design is correct for these properties. Fail → the checker produces the exact violating sequence — far more useful than a production incident report.

NASA’s bounded-loop rule also transfers directly to Streams subscriptions: maxTurns and budgetTokens must be required fields, not optional defaults. An Agent session without explicit caps is an unbounded loop in flight software by another name.

How the layers compose

Three independent layers, each catching what the others cannot.

Layer 1 — Formal methods at design time. Before a line of Rust. TLA+ for the three critical invariants above. The model is the specification; the Rust implements it. Not full formal verification of the entire codebase — that is the shuttle’s cost curve — but formal verification of the three properties where failure is highest: duplicate virtual keys, mutable WORM, stuck cells.

Layer 2 — Rust type system at compile time. Ownership for process-level key uniqueness. Send/Sync for thread isolation. Exhaustive enums for valid cell transitions. Newtype wrappers for domain invariants:

// Provably between 0 and 100 — constructor is the only entry point
pub struct EscrowPct(f64);

impl EscrowPct {
    pub fn new(value: f64) -> Result<Self, ValidationError> {
        if !(0.0..=100.0).contains(&value) {
            return Err(ValidationError::OutOfRange {
                value,
                min: 0.0,
                max: 100.0,
            });
        }
        Ok(Self(value))
    }
    pub fn value(&self) -> f64 {
        self.0
    }
}

Once a value has type EscrowPct, no downstream check is needed. The type is the proof the precondition was satisfied — the ontology near-miss trap from structured recall encoded structurally, not as a runtime query.

#[must_use] on WORM write functions means the compiler warns if a write result is dropped. NASA’s “check all return values” becomes a compiler property. And a failed WORM write must halt the cell: continuing after a failed audit write breaks the core guarantee.

Layer 3 — Runtime assertions at execution time. assert! for production invariants. debug_assert! for expensive checks in development. Checked arithmetic on token budgets. The Armstrong lesson: assertions are not defensive coding. They are executable invariants. When one fails, the cell crashes, the supervisor restarts, the WORM trail records the failure. That is correct behavior — detecting the unexpected and recovering to a known state.

Effect-TS: the same principles on the TypeScript side

clawql-core runs Effect-TS. Same correctness-by-construction thinking, different mechanisms.

Effect<A, E, R> makes errors and dependencies explicit. A function that can fail a precondition returns Effect<A, ValidationError, never> rather than throwing. Callers are forced to handle the error. Weaker than SPARK’s compile-time proof; stronger than unchecked exceptions.

The R parameter is Effect’s approximation of SPARK information-flow contracts. A service that needs VaultClient declares it. It cannot touch VaultClient without having it provided. Every call site can see the dependency:

// Type proves this only touches VaultClient and WormDb
const expireVirtualKey = (
  keyId: VirtualKeyId
): Effect.Effect<void, KeyNotFoundError, VaultClient | WormDb> =>
  Effect.gen(function* () {
    const vault = yield* VaultClient;
    const worm = yield* WormDb;
    yield* vault.expireKey(keyId);
    yield* worm.append({ type: 'VIRTUAL_KEY_EXPIRED', keyId });
  });

Schema is Design by Contract at every data boundary — ontology field extraction as precondition enforcement:

const MatterSchema = Schema.Struct({
  id: Schema.String.pipe(Schema.pattern(/^MAT-\d{4}$/)),
  escrowPct: Schema.Number.pipe(Schema.between(0, 100)),
  nonCompeteMonths: Schema.NonNegativeInt,
});
// Decode is the gate. Invalid data → typed error.
// Valid data carries the proof that it was checked.

STM handles concurrent budget enforcement — two concurrent tool calls cannot race past the budget together because check and deduct are atomic:

const checkAndDeductBudget = (
  key: VirtualKey,
  tokensRequested: number
): Effect.Effect<void, BudgetExhaustedError, never> =>
  STM.atomically(
    STM.gen(function* () {
      const current = yield* TRef.get(key.tokensUsed);
      if (current + tokensRequested > key.budgetTokens) {
        yield* STM.fail(new BudgetExhaustedError());
      }
      yield* TRef.set(key.tokensUsed, current + tokensRequested);
    })
  );

Effect-TS gets you roughly 60–70% of SPARK’s guarantees. The remaining gap — liveness, global fleet invariants, loop termination proofs — is where TLA+ applies, identically to the Rust side.

The agent behavioral contracts connection

Early 2026’s Agent Behavioral Contracts (ABC) formalize what these three traditions imply for autonomous agents: preconditions, invariants, governance, recovery.

That is Design by Contract at the agent layer. Preconditions are ATR scoping — which tools the agent may call. Invariants are the WORM trail — every action recorded before acknowledgment. Governance is Panguard — fail-closed on scope violations. Recovery is the cell’s Terminating state — supervisor restarts to a known state.

The pattern works for flight software and for autonomous agents for the same reason: failures have real consequences, human intervention is delayed or impossible, and the cost of getting it wrong is high.

The practitioner version of the same idea: MCP tools without a promotion-gate architecture are a hallucination amplifier. Findings start as candidates and only promote after gates pass. The hallucination bin is a precondition — nothing enters the knowledge base without proof. Design by Contract applied to agent outputs.

The honest gap

Rust and Effect-TS do not give you what SPARK gives you. Be direct about it:

Property	SPARK/Ada	Rust	Effect-TS
Memory safety	Proved	Proved	N/A
Data race freedom	Proved	Proved	STM / Ref safe
State transition validity	Proved	Type-safe at call site	Type-safe at call site
Information flow isolation	Proved	Visible, not proved	Visible via `R` channel
Liveness (termination)	Proved via model checking	Not achievable	Not achievable
Global fleet invariants	Proved via model checking	Not achievable	Not achievable

The gap closes with TLA+ at design time. The three models above are each around 50–100 lines. TLC runs them in minutes. For most software the remaining gap does not matter. For a TEE that processes regulated data and produces cryptographically verifiable audit trails — including optional QR air-gap export — it does. That is the confidence regulated buyers need when the claim is hardware-verified sessions and a tamper-proof trail.

What this means for building on ClawQL

If you are building on Streams / cellrt / TEE, you are building on a runtime where:

Memory safety and data race freedom are proved by the Rust compiler on every build.
Cell lifecycle transitions are enforced by the type system — you cannot skip from Spawning to Dead without the compiler refusing.
Critical fleet invariants are verified by TLA+ before the code ships.
Virtual key lifecycle is enforced by Drop — the key expires when the cell drops, regardless of why.
The audit trail is append-only by construction — LTX acknowledges writes only after they are durable in the bucket.
The WASM capability sandbox is enforced by the WIT world — undeclared capabilities are not linked, so they do not exist.
On the TypeScript side, every data boundary is validated by Effect Schema; every capability dependency is declared in R; every concurrent state mutation goes through STM.

These are not features bolted onto an otherwise unverified system. They are the structure of the system. Armstrong, Jane Street, and NASA all came to the same conclusion: at the level of infrastructure where failures have real consequences, correctness has to be built in, not added on.