A microkernel where nothing runs unless it can prove itself.
Every program on NONOS is a signed, sandboxed capsule that carries a transparent, post-quantum proof of what it is and what it is allowed to touch. The kernel checks that proof before every spawn, and the bootloader checks the kernel the same way before it jumps. There is no unsigned path to execution, no debug switch that turns the check off, no privileged account that can wave code through. Trust flows one direction only, downward from a root you can read.
NONOS is written in Rust, capability-based, and RAM-resident: it keeps no mutable state on disk and leaves nothing behind after power-off. That is the ZeroState model the system is named for. It targets x86_64, ARM64 and RISC-V; x86_64 is the production tree, the other two are architecture-ready backends behind the same arch boundary.
It boots. The default image comes up to a graphical desktop with a damage-tracked compositor, window management, a terminal and a file manager, on real drivers for NVMe and AHCI storage, xHCI USB and mass storage, e1000 and Realtek networking, Intel and Realtek Wi-Fi, HDA audio, i2c and PS/2 input. Around sixty capsules ship in it. One command builds the whole system, proves it, and boots it.
The attestation is checked, not asserted. Four independent tools verify it on every change: Lean 4 with 203 theorems, Verus, Kani, and 165 runnable proofs against the real code. The prover and the verifier are a single crate linked into both the kernel and the bootloader, so the proof that gets written is the proof that gets read.
The full reference is the NØNOS documentation wiki, mounted at docs/ as a submodule so a checkout always carries the matching revision. It is written against the source tree, with file and line references, so every claim can be checked against the code. Start with the architecture overview, then the verification scope and the attestation model.
The common tasks each have a short guide in the wiki:
The quickstart
goes from a clean checkout to the system booting in QEMU.
Configuring a kernel
assembles your own kernel with make menuconfig.
Contributing
is where to start;
verifiable work
is the capsule path.
Reporting
covers security reports and scope, and
rewards
covers what securing NONOS pays.
Design discussion, capsule work and security reports start there. Verified contributors get the capsule-signing channels.
make # the full ZeroState system, attested, as a bootable image
make qemu # boot it in QEMU
make menuconfig # choose what goes in your kernel
make from-config # build that
AGPL-3.0-or-later. Redistributable device firmware is not part of the source and carries its own terms.