README.md

---
license: other
license_name: snapkitty-tri-license
license_link: https://huggingface.co/Snapkitty/sovereign-agi-kernel/blob/main/LICENSE
tags:
- snapkitty
- agents
- idris2
- lean4
---

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

# Sovereign AGI Kernel

**The first AGI kernel where correctness is enforced by the type system, not by monitoring.**

Built by Ahmad Ali Parr. Formalized in Idris 2 + Lean 4. Zero `sorry`. Zero runtime exceptions for the invariants that matter.

---

## What This Is

Most AI systems trust their own output. This one can't.

Every mathematical claim from any AGI component must pass through a formally verified kernel before it is accepted. The kernel is written in Idris 2 — a dependently-typed language where the **type checker IS the proof checker**. If it compiles, the invariants hold. Not because we tested them. Because violating them is not a valid program.

```
AGI Component
     |
     v
Reasoning_IDL.verifyClaim()   <- only path to acceptance
     |
     v
SovereignKernel (Idris 2)     <- entropy-bounded, WORM-audited
     |
     v
WORM Audit Chain              <- append-only by construction
     |
     v
ACCEPTED or REJECTED
```

There is no other path.

---

## The Five Axioms

All five are **types**, not policies. They cannot be violated at runtime — they cannot be expressed in the type system at all.

| Axiom | What it means |
|-------|--------------|
| **1. Entropy bound** | `EntropyBound n = LTE n 20` — compile-time. Violating it is not a runtime error. It is a type error. |
| **2. Active ⇒ Trusted** | `Agent Active Untrusted` is an uninhabited type. No constructor exists. Cannot be instantiated. |
| **3. Artifact = Proof** | `%default total` on all Idris files. No `sorry`. No incomplete matches. Compiles = verified. |
| **4. WORM append-only** | `WORMChain` has no `Remove` constructor. Deletion is not prevented — it does not exist. |
| **5. Kernel is sole trust anchor** | No import path from untyped code to kernel internals. Structurally impossible to bypass. |

---

## Architecture

```
sovereign-agi-kernel/
|-- idris/
|   |-- AgentModel.idr        <- Active=>Trusted by construction
|   |-- WORM_Audit.idr        <- Append-only hash chain (no Remove)
|   |-- Reasoning_IDL.idr     <- Formal interface (only path to kernel)
|   `-- SovereignKernel.idr   <- Entropy-bounded reasoning oracle
|
|-- lean/
|   `-- Erdos/                <- Lean 4 proofs (DSS greedy bound)
|
|-- runtime/
|   |-- greedy.mjs            <- DSS cardinality oracle
|   |-- fault-isolation.mjs   <- 98% search reduction via DSS
|   |-- network-tomography.mjs <- Constant-size packet count
|   |-- threshold-crypto.mjs  <- Signer count without identity
|   `-- financial-forensics.mjs <- Anti-structuring channel count
|
|-- scaffold/
|   `-- agi_gate.py           <- Python integration (kernel-gated reasoning)
|
|-- sovereign/scripts/
|   |-- build_sovereign.sh    <- Idris 2 + Lean 4 build
|   |-- validate_entropy.sh   <- Entropy bound verification
|   `-- commit_to_worm.sh     <- WORM seal
|
|-- FORBIDDEN/                <- Zones that invalidate ValidationProof
|-- ROOT_CLAIMS.md            <- 5 non-negotiable axioms (all are types)
|-- CI_SOVEREIGN.yml          <- 5-stage pipeline
|-- Dockerfile                <- Air-gapped multi-stage build
`-- Makefile                  <- Local dev targets
```

---

## The DSS Oracle

The runtime implements a **Distinct Subset Sum (DSS) cardinality oracle** — a formally proved combinatorial engine that determines cardinality from aggregate sums without enumerating members.

Four production applications:

| Application | What it solves |
|-------------|---------------|
| **Fault Isolation** | Interaction order from test signal — 98% search reduction |
| **Network Tomography** | Packet count from aggregate ACK — constant-size |
| **Threshold Cryptography** | Signer count without identity — privacy + soundness |
| **Financial Forensics** | Channel count for anti-structuring detection |

All four are formally bounded by the Erdős-Straus greedy bound, proved in Lean 4.

---

## Run It

```bash
# Build the Idris 2 kernel
make idris

# Run entropy validation
make verify

# Run DSS oracle (all 4 applications)
cd runtime && node main.mjs

# Run Python AGI gate integration
python scaffold/agi_gate.py

# Seal to WORM
make seal

# Full pipeline
make gate
```

---

## CI Pipeline (5 stages)

```
Stage 1: FORBIDDEN zone check     <- Fails if banned patterns detected
Stage 2: Idris 2 kernel build     <- Fails if types don't hold
Stage 3: Entropy bound validation <- Fails if H > 0.20
Stage 4: Runtime oracle tests     <- Fails if DSS oracle wrong
Stage 5: WORM commit              <- Seals artifact hash on success
```

If Stage 2 fails, the kernel invariants are violated. The build does not proceed.

---

## Why Idris 2

Every other AGI safety approach uses one of:
- Runtime monitors (can be bypassed)
- Test suites (can miss edge cases)
- RLHF alignment (can drift)
- Constitutional AI (enforced by another model)

Idris 2 uses **dependent types** — the specification and the implementation are the same artifact. You don't write a spec and then test that the code matches it. The code that doesn't match the spec **does not compile**.

The kernel cannot hallucinate its own invariants. The type checker would reject it before you could run it.

---

## Mathematical Foundation

- **Erdős-Straus Conjecture** — DSS greedy bound (Lean 4 formalized)
- **Dependent Type Theory** (Martin-Löf) — Idris 2 type system
- **Entropy Bound** — fixed-point arithmetic, compile-time verified
- **WORM Chain** — append-only linked structure, deletion impossible by type

---

## Who Built This

**Ahmad Ali Parr** — Haskell, Idris 2, Lean 4, Agda, Prolog, APL, Coq. UCSD Liquid Haskell contributor. No PhD. Types compile. `refl` doesn't negotiate.

The kernel is not an experiment. It is not a demo. It is the trust anchor for sovereign AGI.

---

## License

**Tri-License** (BSL-1.1 / AGPL-3.0 / MPL-2.0) — See [LICENSE](LICENSE)

- SaaS/network deployment: AGPL-3.0 (mandatory, no opt-out)
- Enterprise/commercial: BSL-1.1 (converts to AGPL-3.0 after 2028-08-15)
- File-level modifications: MPL-2.0 (non-network only)
- Patent retaliation clause active

Copyright (C) 2026 Bel Esprit D'Accord Irrevocable Trust / SnapKitty Collective Limited

### 💼 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-agi-kernel)** · A.parr@belespritdaccord.uk