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