The sovereign stack

Technology

Engineering announcements, formal proof reports and deep-dives across the sovereign stack. The work behind the inventory.

Engineering writing

janus · proof

After the Borrow Checker

Rust proved that programmers would accept compiler-enforced discipline for memory. Janus asks why memory should be the only truth the compiler can see – and the Sovereign Society Foundation has now bound seven Janus disciplines to machine-checked Lean4 proofs.

Markus Maiwald
libertaria · proof

Three Theorems for a Quantum-Safe Identity

SKH v2 now ships with machine-checked Lean4 proofs for every LaBRADOR claim it makes – Recovery, Membership, Derivation – under explicit Module-LWE and Module-SIS axioms. The Sovereign Society Foundation has bound the lattice lane to a clean axiomatic contract, ready for the LaZer/LaBRADOR graft.

Markus Maiwald

Explore the stewardships