Snapkitty/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

# 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

• 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