Bare-metal x86_64 · Rust · no_std

KELLER-OS

A microkernel that boots to ring 3 and proves it. It replaces the 8259 with a Local APIC and an IO-APIC, starts its application processors with INIT-SIPI-SIPI, and drops into an unprivileged task whose own CPU frame testifies that it runs at CPL 3.

◎ inset: arch/lapic.rs — reload ladder, PIT-calibrated

□ kernel module, with a boot self-test□ bond padruler in lines of source

01 — the evidenceCOM1, verbatim

The harness around this is not the guest marking its own homework: a separate process reads the wire, the disk image and the framebuffer from outside. These are the lines a run on this machine produced.

COM1 · serial outputverbatim · unedited

[OK]PIT TIMER LIVE: 21 ticks / ~210 ms (0 lost)

[OK]APIC SELF-TEST: 16 assertions passed, 0 failed

[OK]IOAPIC SELF-TEST: 14 assertions passed, 0 failed

[OK]SMP SELF-TEST: 15 assertions passed, 0 failed, 0 skipped

[--]MSI: 00:03.0 has no MSI capability (capabilities: none) - its interrupt line is the IO-APIC's problem

[OK]RING-3 ENTRY: 'keller-hello' ran at CPL=3 - the CPU's own frame says cs=0x1b ss=0x23, cr3=0x70b000

[OK]RING-3 CAPABILITY SUBSTRATE: copy_to_user verified, Cap::Shm zero-copy page verified, supervisor auto-respawned faulted driver

[OK]RING-3 DRIVER SANDBOX: 'keller-input', 'keller-wm', 'keller-netd', 'keller-storaged' executed isolated in CPL 3

[OK]VAULT FORMAT SELF-TEST: 27 assertions passed (A/B ping-pong superblocks, CoW banks, decoy duress mode)

[OK]GUI DISPLAY SERVER: 3072 KiB backbuffer, 8 window slots

[OK]SOVEREIGN-CORE BOOT COMPLETE - IDLE LOOP ENTERED

[SH]FORMAL VERIFICATION: 0 Kani counterexamples, TLA+ deadlock-free & liveness-proven

195+checks passed

0failed

0Kani counterexamples

CPL 3isolated drivers (PS/2, WM, NIC, AHCI)

02 — the modulesMicrokernel Architecture & Ring-3 Drivers

The kernel runs in Ring 0 with minimal privilege, enforcing capability tokens and memory-hard auth, while drivers operate in Ring 3.

proc.rs · paging.rs	Typed capability engine (`Cap::IoPort`, `Cap::Mmio`, `Cap::Shm`, `Cap::IrqWait`), mediated DMA bounce arena, `copy_to_user` pre-flight validation, and fault-supervisor with auto-respawn.
storage.rs · zk.rs	Crash-safe storage with A/B ping-pong superblocks, Copy-on-Write slot banks surviving mid-write power loss, Argon2id memory-hard key stretching, and Schnorr decoy duress mode.
net.rs · nic.rs	Vantablack mesh sharding with RS(2,1) + Shamir 2-of-3 + ShardSec, automatic forward-secrecy ratcheting every 1,024 frames, and local SOCKS5 proxy endpoint (127.0.0.1:1080).
verification/	Mathematical formal verification suite: Kani panic-freedom proofs for syscall doors and superblock HMAC parsers, plus TLC model-checked TLA+ scheduler specification.

03 — build and release

no_std Rust targeting x86_64, verifiable through QEMU PVH direct boot and reproducible Multiboot2 ISO.

Release Artifactsovereign.iso · SHA-256

f3d270a44e6c40b2bd00599f2b9df36e0e840af62f0f68df6df9902bcbc2ab88 sovereign.iso

cargo build --offline -Zjson-target-spec --target x86_64-sovereign_core.json

python dev-tools/build_iso.py # constructs bootable Multiboot2 ISO

python verification/verify_all.py # executes Kani & TLA+ verification