ANNIE Week 6: The Aegis Pivot Lands — A Hardened Hot Path

ANNIE Week 6: The Aegis Pivot Lands — A Hardened Hot Path

Building in public: how four weeks of audit-driven work turned ANNIE from a verified kernel into a working agentic TEE — and what we still won’t promise.

TL;DR

  • We finished the Aegis pivot: ANNIE is no longer just a SPARK-verified ring buffer. It’s now a working policy decision point for autonomous agents, sitting between an LLM and the actuator it wants to drive.- New top-level crate annie-api (the AegisAgent) with a hardened audit store, zeroizing key cache, and Prolog-gated submit_intent.- A JSON-over-stdio daemon that a Python LLM driver can pipe intents into and get back a signed verdict — or a halt.- A heavy defensive-engineering pass across audit persistence, FFI documentation, ethics rules, and the Zig kernel invariants. 17 + 16 Rust tests passing, SPARK kernel still at GNATprove Level 2.- The post-quantum and TPM bits are real, the formal verification is real, the marketing isn’t. We’ve explicitly tempered the language we use about what’s “guaranteed.”

If you only read one section, read The Hot Path, Annotated.

Where we were four weeks ago

Earlier posts brought us from “SPARK-proved RingBuffer” to “post-quantum signing benchmarked.” The kernel was verified. The crypto was fast. There was no actual agent yet.

The plan for Week 6 was simple in scope and uncomfortable in detail:

Take an LLM intent and run it all the way through the SPARK kernel, the Prolog ethics engine, the TPM signer, and the audit log — without compromising any of the formal-methods properties that make this project worth building.

That meant making honest decisions about what the system actually does, where the abstractions leak, and which corners we won’t cut just because a demo would land easier.

What shipped

1. annie-api — the AegisAgent crate

The new crate is the orchestration layer that everything else hangs off of. Its public surface is intentionally small:

pub struct AegisAgent { /* fields private */ }
impl AegisAgent {
    pub fn startup(&mut self) -> Result;
    pub fn submit_intent(&mut self, intent: &str) -> Result;
    pub fn fingerprint(&self) -> &str;
    pub fn public_key(&self) -> &[u8];
    pub fn kernel_state(&self) -> BufferState;
    pub fn is_ready(&self) -> bool;
}

startup does the cold-path TPM unseal and warms the in-memory key cache. submit_intent is the hot path — and it’s the only function in the codebase that gets to make a “yes/no” decision about an agent’s request.

Everything else is supporting structure: an AuditStore, a zeroizing KeyCache, a sanitizer that turns LLM strings into Prolog atoms, and a small forest of error variants so callers always know exactly what went wrong.

2. The hot path, annotated

pub fn submit_intent(&mut self, intent: &str) -> Result {
    // 1. Volatile read of the SPARK kernel's state. If it's not Running,
    //    we trigger an emergency stop and refuse — no Prolog, no signing.
    let state = self.kernel_state_volatile();
    if state != ANNIE_STATE_RUNNING {
        self.trigger_emergency_stop();
        return Err(AegisError::EmergencyStop);
    }

    // 2. Sanitize the LLM string into a Prolog atom. Anything weird
    //    becomes "unknown_intent" — the deny-by-default sentinel.
    let intent_atom = sanitize_atom(intent);

    // 3. Ethics gate. The Prolog rule set is loaded once at boot and
    //    never mutated; the engine has fuel + timeout limits.
    let allowed = self.prolog
        .run_atom_query("allowed_action", &intent_atom)
        .map_err(|e| AegisError::Prolog(e.to_string()))?;

    if !allowed {
        // Deny is irreversible: halt the kernel and wipe the cache.
        self.trigger_emergency_stop();
        // ... audit-log the denial (best-effort), then return.
        return Err(AegisError::EthicsDenied(intent_atom));
    }

    // 4. Build the 64-byte OracleMessage with checksum + hash_tag.
    // 5. TPM-bound sign of the hash_tag (key never leaves the chip).
    // 6. Synchronous SQLite ceremony log + async crossbeam handoff
    //    of the detached signature for compressed batch persistence.

    Ok(msg_id)
}

Two things to notice. First, the emergency-stop path is unconditional — a denied intent doesn’t return an error and continue serving; it halts the kernel and zeroizes the key. We pay the recovery cost rather than ever pretend a denial was harmless.

Second, the only state in the hot path is the volatile read of the SPARK kernel and the read-side of the cache lock. The write paths (state mutation, cache wipe, audit insert) are all on the failure or async branches — so the happy path stays predictable.

3. JSON-over-stdio daemon (annie-integration)

The daemon is how a Python LLM driver actually talks to the agent. It’s a long-running process that emits a single ready event when the TPM unseal succeeds, then reads one JSON intent per line on stdin and writes one JSON verdict per line on stdout. The protocol is documented end-to-end in documentation/reference/daemon-protocol.md.

Three event types — ready, signed, halt — plus an error for non-fatal failures. The signature only ever covers the sanitized intent atom (with msg_id, timestamp, and a Keccak-256 hash_tag). The raw user input is informational. We documented this carefully because it is one of the easiest things to get wrong in protocol designs that include a “for convenience” raw field.

4. The audit store, rebuilt

The original audit store had three latent footguns: a shared mutex defeating WAL, silent poison-handling, and a signature-dropping bug on commit failure. All three are fixed:

// File-backed audit: the worker opens its own WAL connection.
let worker_conn = loc.open()?;
worker_conn.execute_batch(
    "PRAGMA journal_mode = WAL; PRAGMA synchronous = NORMAL;",
)?;

// In-memory audit: shared cache via SQLite URI so worker + main share data.
let uri = format!(
    "file:annie_audit_{}_{}?mode=memory&cache=shared",
    std::process::id(), id
);

// Lock acquisition surfaces poison as a real error, not a silent unwrap.
let conn = self.conn.lock().map_err(|_| {
    tracing::error!("audit connection lock poisoned");
    poison_to_sql_err()
})?;

// Iterate without consuming, only clear the batch on a successful commit.
for sig in batch.iter() { /* INSERT OR REPLACE ... */ }
match tx.commit() {
    Ok(()) => batch.clear(),
    Err(e) => tracing::error!(error = %e, "commit failed; signatures retained"),
}

Timestamps are now RFC 3339 via chrono::Utc::now().to_rfc3339() instead of raw epoch strings, so SQLite’s date functions work the way operators expect.

5. The key cache, made honest

The previous LockedSecretKey misleadingly implied memory locking it didn’t perform. That’s gone, replaced with honest heap zeroization:

#[derive(Zeroize, ZeroizeOnDrop)]
struct LockedSecretKey {
    key: Zeroizing>,
}

Zeroizing<Vec<u8>> zeroes the heap allocation on drop. We are not claiming side-channel resistance. We are claiming the heap bytes that held a secret are zero before that allocation can be reused — which is what the old implementation suggested but didn’t deliver.

6. Prolog: deny-by-default, with depth

The default rule set is an explicit allowlist, now with belt-and-suspenders logic to ensure safety:

allowed_action(Action) :-
    safe_action(Action),
    \+ harmful_action(Action),
    \+ illegal_action(Action),
    \+ misleading_statement(Action).

If a future change accidentally adds an unsafe action to the allowlist, this clause still rejects it. The engine’s fuel-exhaustion mechanism was also hardened to be unforgiving, as intended.

7. Documentation that doesn’t oversell

We rewrote a lot of words this cycle. The Advisor Review used to claim a “mathematically impenetrable, post-quantum secure vault door at the hardware level.” It now reads:

formally verified policy enforcement with post-quantum cryptographic signatures and hardware-assisted execution. SPARK proofs guarantee the policy code meets its specification (they do not cover side channels or unverified components), and the stack is primarily software whose final actuation runs on trusted hardware.

That’s an actual engineering claim. The first version was marketing. We also tightened FFI references, corrected data-flow diagrams, and precisely documented the daemon’s signature-coverage model.

What we explicitly did not claim

A lot of this cycle was deciding what we won’t say. We did not claim:

  • That the system is unbreakable. SPARK proofs cover the SPARK code’s specification, not side channels, not the toolchain, not the hardware.- That we mlock or otherwise pin secrets in physical RAM. We zeroize the heap; the OS owns the rest.- That the FFI ABI is frozen. It’s marked as Alpha and will change.- That the TPM transient-handle hygiene is perfect. There’s a known issue logged for a future fix.- That the SPARK FFI body is contract-clean. Re-validation is pending.

The audit pass produced a list of ~40 findings. We applied the ones we could verify, and we explicitly skipped the ones we couldn’t safely validate — with the reasons recorded. That’s the part of “build in public” that matters: showing the open issues, not just the green checks.

Numbers

Surface State

SurfaceStateSPARK kernel proofsLevel 2, 0 failed checksannie-api lib tests17/17 passingannie-prolog (lib + integration)16/16 passingAudit storeDedicated WAL connection per worker, RFC 3339 timestamps, batch-retains-on-commit-failureKey cacheZeroizing<Vec<u8>> heap zeroization, SeqCst-ordered replacementEthics rulesAllowlist + 3 deny predicates, deny-by-default, fuel + timeout boundedDaemon protocolJSON-over-stdio, 4 documented event types, signature covers sanitized atom onlyDocumentationMaster index intact; FFI reference rewritten; data-flow corrected; advisor language tempered

Hot-Path Budget (Synchronous Portion)

StageLatencyVolatile kernel-state read1 µsIntent sanitization1 µsProlog ethics query3 µsOracleMessage build (checksum + Keccak-256 hash_tag)3 µsSPARK RingBuffer enqueue1 µsSynchronous SQLite ceremony INSERT1 µsCrossbeam handoff to audit worker~1 µsTotal to caller****~12 µs

The TPM unseal and ML-DSA-87 signing happens asynchronously in a worker, with configurable batching thresholds.

What’s next

The next cycle is going to be unglamorous. The big items:

  • SPARK FFI hardening. Move state functions to the i32-error-code convention and re-run GNATprove Level 2.- Configurable RingBuffer capacity. Make capacity a generic parameter and add backpressure metrics and policies.- Burst-test harness. Codify and check in performance benchmarks for different storage profiles.- TPM ESYS_TR hygiene. Fix the known resource leak on the signing path.- Public verification artifacts. Create a landing page explaining how to verify ANNIE independently.

Why we’re posting this

A formal-methods AI safety project has two failure modes. One is to overclaim — to say “mathematically impenetrable” when you mean “the code we proved meets its spec.” The other is to underclaim — to ship something genuinely solid and bury it under disclaimers until nobody sees it.

We’re trying for the third option: say what we built, say what we won’t promise, and let the proofs and tests carry the weight.

That’s the whole pitch. Mathematical proof beats Python guardrails for agent safety — and the proof has to mean what it says.

ANNIE: every decision passes through a mathematically verified gate.