Building a Production-Grade epistemic Firewall: ANNIE Week 2 Progress

An agent CAD foundation built on formal methods, verified at mathematical proof level.

The Challenge

Most AI systems today lack a provable safety foundation. Neural networks make decisions that are fundamentally uninterpretable. We wanted something different: a kernel where every operation can be mathematically proven safe.

Week 2 Achievement: Rust FFI Bridge

We’ve completed the Rust foreign function interface (FFI) bridge connecting our SPARK/Ada kernel to Rust.. the language we’ll use for orchestration and external integrations.

What We Built

1. Memory Layout Verification

• OracleMessage: 64-byte C-compatible struct matching Ada record layout
• Offsets verified: msg_id(0), timestamp(4), payload(8), checksum(56)
• RingBuffer: 16-message queue (1048 bytes)

2. FFI Protocol

extern "C" {
    pub fn annie_init(buffer: *mut RingBuffer);
    pub fn annie_push(buffer: *mut RingBuffer, msg: OracleMessage);
    pub fn annie_pop(buffer: *mut RingBuffer, msg: *mut OracleMessage);
    pub fn annie_peek(buffer: *const RingBuffer, msg: *mut OracleMessage);
    pub fn annie_clear(buffer: *mut RingBuffer);
}

3. Contract-Verified Operations All SPARK operations carry mathematical Pre/Post contracts proven by GNATprove:

procedure Push (Buffer : in out RingBuffer; Msg : OracleMessage) with
  Pre  => not Is_Full (Buffer),
  Post => Get_Count (Buffer) = Get_Count (Buffer'Old) + 1;

This means: before you can push, the buffer must not be full. After push, the count must increase by exactly one. These aren’t runtime checks.. they’re mathematical theorems proven at compile time.

Verification Results

running 2 tests
test verify_ringbuffer_layout ... ok
test verify_oracle_message_layout ... ok

Workspace Integration

$ cargo build --workspace
Finished `dev` profile [unoptimized + debuginfo] target(s) in 1.11s

Why This Matters

Traditional AI safety tries to add guardrails after deployment (RLHF, constitutional AI). They’re probabilistic, incomplete, and unverifiable.

Our approach builds the safety foundation first:

• Every push/pop operation proven safe at level 2
• No buffer overflow possible (mathematically proven)
• No race conditions on state transitions
• Every FFI boundary verified

This is what formal methods practitioners have known for decades: prevention is better than detection.

What’s Next

Week 3: Emergency Stop System with:

• Atomic kill (CAS) in SPARK
• Graceful shutdown contracts
• Sub-100ms halt timing requirements
• JSON state snapshots for crash recovery

Project Status

Total commits this session: 7 atomic changes Test coverage: 2 passing tests Lines changed: ~200 (Ada + Rust + Protocol docs)

We’re building the epistemic firewall for agentic AI — where every decision passes through a mathematically verified gate.