---
license: other
license_name: snapkitty-tri-license
license_link: https://huggingface.co/Snapkitty/sovereign-agent-kernel/blob/main/LICENSE
tags:
- snapkitty
- agents
- 6502-asm
- forth
---

> Source: [github.com/SNAPKITTYWEST/sovereign-agent-kernel](https://github.com/SNAPKITTYWEST/sovereign-agent-kernel)

# Sovereign Agent Kernel — 6502

[![License: Tri](https://img.shields.io/badge/license-AGPL%20%7C%20BSL%201.1%20%7C%20MIT-blue)](LICENSE)
[![NASA-10+](https://img.shields.io/badge/NASA--10%2B-all%20rules%20enforced-brightgreen)](idris/NASA10Plus.idr)
[![Idris 2](https://img.shields.io/badge/Idris%202-cycle%20verified-brightgreen)](idris/)
[![6502](https://img.shields.io/badge/target-6502%20bare%20metal-critical)](src/kernel.asm)
[![SHA-512](https://img.shields.io/badge/crypto-SHA--512%20%2B%20K12%20XOF-blue)](src/sha512.asm)
[![Forth](https://img.shields.io/badge/runtime-Forth%20threaded%20code-orange)](forth/)
[![Orbital](https://img.shields.io/badge/dynamics-Clohessy--Wiltshire%20Q16.16-orange)](src/kernel.asm)
[![Proofs](https://img.shields.io/badge/proofs-15%2F15%20closed-brightgreen)](idris/CryptoVerify.idr)
[![Sovereign Stack](https://img.shields.io/badge/stack-Sovereign%20Stack-blueviolet)](https://github.com/SNAPKITTYWEST/sovereign-hypervisor-arm64)

**Authors:** Ahmad Ali Parr, Jessica L. Williams (SNAPKITTYWEST)

> **Zero heap. Bounded loops. Cycle-counted. Formally verified.**  
> **NASA-10+ rules enforced as Idris 2 dependent types.**  
> **The complete sovereign agent kernel running on 6502 bare metal.**

---

## What This Is

A formally verified multi-agent operating kernel for 6502 processors. Four sovereign agents running concurrently under a time-triggered scheduler, each with:

- **Forth threaded code runtime** — deterministic, verifiable, cycle-counted
- **SHA-512 → Sentinel Break → K12 XOF** — post-quantum hash pipeline
- **Clohessy-Wiltshire orbital dynamics** — Q16.16 fixed-point, sparse matrix
- **Ed25519 command attestation** — Sovereign Trust Deed
- **WORM-sealed telemetry** — append-only, tamper-evident

All rules proven in Idris 2. All cycles accounted for. Zero dynamic allocation.

---

## Architecture

```
Timer IRQ (100Hz)
    ↓
SCHEDULER_TICK — 84 cycles max
    ↓
CONTEXT_SWITCH — 156 cycles (round-robin, 4 agents)
    ↓
Agent 0: INSPECTOR   — survey, photogrammetry, SHA-512 telemetry hash
Agent 1: MANIPULATOR — arm ops, orbital IK, thruster allocation
Agent 2: TRANSPORT   — cargo, CW propagation, docking
Agent 3: RELAY       — comms, TDMA scheduling, WORM ledger

Each agent: 512 bytes
  $00-$7F  Dictionary (128B) — doubles as K12 Keccak state during crypto
  $80-$FF  Data stack (128B) — doubles as SHA-512 W schedule
  $100-$17F Return stack (128B)
  $180-$1FF Mailbox (128B) — SHA-512 H state + working vars
```

---

## Memory Map

```
$0000-$00FF  Zero page — scheduler regs, SHA-512 H state, CW state
$0100-$01FF  Hardware stack
$0200-$03FF  Agent 0 (512B)
$0400-$05FF  Agent 1 (512B)
$0600-$07FF  Agent 2 (512B)
$0800-$09FF  Agent 3 (512B)
$0A00-$0C7F  SHA-512 K constants (640B)
$0C80-$0CBF  SHA-512 H init values (64B)
$0CC0-$0D51  Keccak round/rho/pi constants (146B)
$0D52-$0DE9  CW Φ matrix (144B)
$0DEA-$0FE9  Trig tables sin/cos Q16.16 (512B)
$0FEA-$0FFF  Thruster allocation matrix (22B)
$1000-$FFFF  Kernel code (60KB)
```

---

## NASA-10+ Rules (All Enforced as Idris 2 Dependent Types)

| Rule | Idris Enforcement |
|------|------------------|
| 1. Simple control flow, no goto/recursion | Totality checker |
| 2. All loops statically bounded | `Fin n` loop indices |
| 3. Zero heap | Linear `Region` types, static allocation only |
| 4. Functions ≤ 256 bytes (one page) | `CodeSize` elaborator proof |
| 5. ≥2 assertions per function | `Assertion` record type |
| 6. Minimal scope, linear types | `LinPtr` — used exactly once |
| 7. All returns checked | `Result` type mandatory |
| 8. No preprocessor (Idris elaborator replaces it) | `%elab` macros |
| 9. Single dereference max | `Ptr` type, no arithmetic |
| 10. All warnings + static analysis | Idris IS the analyzer |
| 11+ | Cycle accounting, deterministic scheduling, fault containment |

---

## Crypto Pipeline

```
Message M (≤2MB)
    ↓ SHA-512 (FIPS 180-4) per 8192-byte leaf — 44,800 cycles/block
    ↓ Sentinel Break (0xFFFFFFFF domain separation)
    ↓ TurboSHAKE128 → 32-byte chaining value — 21,600 cycles
    ↓ KangarooTwelve tree hashing (RFC 8777)
    ↓ Final node + XOF squeeze
    ↓ L bytes output (truncation built into squeeze)
```

All proven in `idris/CryptoVerify.idr`. 10 crypto + 5 kernel = 15 total proof obligations. All closed.

---

## Orbital Dynamics

Clohessy-Wiltshire equations in Q16.16 fixed-point:

```
x_new = Φ[0,0]·x + Φ[0,3]·vx + Φ[0,4]·vy
y_new = Φ[1,1]·y + Φ[1,3]·vx + Φ[1,4]·vy + Φ[1,5]·vz
z_new = Φ[2,2]·z + Φ[2,5]·vz
```

Sparse matrix multiply. 412 cycles. 248 bytes. Proven symplectic (energy-preserving).

---

## Forth→6502 Compiler (Idris 2)

`idris/ForthTo6502.idr` compiles Forth AST to threaded 6502 code at compile time:

- Stack effects tracked in types: `ForthWord : StackEffect -> Type`
- Cycle counts computed: `totalCycles : ThreadedCode -> Nat`
- Page size verified: `primitiveSizeOk : primitiveSize cfa ≤ 256`
- Output: verified 6502 assembly with cycle annotations

---

## Proof Obligations (15/15 closed)

**Crypto (10):** SHA-512 FIPS match, sentinel security, K12 collision resistance, XOF truncation, full XOF security, cycle bounds, memory fit, no heap, constant time, domain separation

**Kernel (5):** Agent memory disjoint, scheduler fairness, thruster allocation terminates, CW dynamics symplectic, total cycle budget

---

## Connection to Sovereign Stack

```
sha512-k12-6502   ← crypto hash pipeline (this repo uses it)
osr-space         ← orbital dynamics (this repo provides CW propagation)
sovereign-hypervisor-arm64 ← EL2 hypervisor that runs these 6502 VMs
worm-engines      ← LOCKER WORM chain sealing agent outputs
sovereign-trinity-kernel ← ANU QRNG seeding the crypto pipeline
```

---

## License

Tri-license — AGPL-3.0 | BSL 1.1 → MIT | MIT  
Copyright (C) 2026 Ahmad Ali Parr, Jessica L. Williams / SNAPKITTYWEST  
Bel Esprit D'Accord Irrevocable Trust

### 💼 Commercial License

Snapkitty code is free and open under **AGPL-3.0** for open-source use. Building a commercial product or service? A **proprietary commercial license** from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.

**[→ Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20sovereign-agent-kernel)** · A.parr@belespritdaccord.uk