An operating system where every program runs in a box.
The box is a short list in the program's signed listing, and every call the program makes is checked against it.

Install it · Using NØNOS · 0.9.3 release notes · Build it · Security limits

A box lists what a program may touch: a window, its own home folder, the network over Nym or Anyone, a terminal, the right to start other programs. Anything not on the list is refused, and the log says why. The kernel sends every Linux call to one supervisor, which holds the box and checks it, and gives the program no rights of its own. Around that the machine has what a daily system needs: a desktop, a browser, a terminal, a wallet, a local model, and a Marketplace of 31 Linux programs. Memory is wiped when you power off, and nothing is written to a disk unless you install.

0.9.3 is the release where those Linux programs get their own windows on the NØNOS desktop. Every claim on this page points at code or at evidence in the tree, and what 0.9.3 does not do yet is under Where 0.9.3 stands.

The boot checks the kernel's STARK proof before it starts anything. This one ran under KVM, which has no TPM, and the screen says so.	A live session says it keeps nothing: files, settings and models are gone when the machine stops. Install NØNOS to keep them.

First-boot setup, one screen at a time:

Pick a keyboard layout. Ctrl+Alt+Space switches layouts at any time.	Name the account.	Choose the network the machine's traffic leaves through: the Nym mixnet, the Anyone onion network, or direct.
What the machine does without being asked: a random MAC address at each start, memory wiped at shutdown, and no telemetry because there is no switch for it.	Choose which wallpapers are kept in the session and which is the desktop's.	Pick a Qwen model that fits this machine's memory, or none.
Turn the desktop apps on or off: browser, wallet, App store, files, editor, media, Linux programs.	Decide whether software installed here may run, or only NØNOS software.	Review the choices before the desktop starts.

The Marketplace lists each Linux program with what it is and what its box allows.	KeePassXC, a Linux program, in its own window. Its box has a window and a home folder and no network.
The NØNOS Wallet. Its first screen says the keys are made on this machine and never leave it.	Settings shows the network the machine is using, and changes it.

audit lists every process with its grants. Kernel threads show as not in the registry, with no signed ceiling recorded.

Figure 1. What a program can reach. Sources: docs/using/linux-box.md, docs/using/marketplace.md.

Each row below is a real attempt from inside a Linux program on the sealed 0.9.3 image, and the answer it got. The recorded run, with every command and screenshot, is in docs/release-evidence/0.9.3/kvm-box-refusals. The file, process and keyboard rows ran in the default box, which is what a program with no listing gets: a terminal, its own home and the right to start programs, with no network. The refused program launch is from Telegram, which runs in the box its listing names.

These are single attempts from inside an app, not an exploit chain. Nobody here claims the box cannot be broken. Security limits lists what the design does not cover.

linux --box runs a Linux program, or one a model wrote, in a sealed box and prints everything the box refused:

linux --box strict sh -c 'echo ok > /tmp/out; echo no > /home/out; nc 10.0.0.1 80'
linux --box offline python3 script.py
linux --box allow:/tmp/out,net:api.example.com:443 python3 agent.py

strict has no network and writes only to /tmp. An allow: box names its folders and, if it needs any, its network destinations, and a connection anywhere else is refused and counted. linux --box learn runs a program once and writes the tightest box file that would let it do what it did. See Run a program in a box.

Counted from git at the commit where the 0.9.2 changelog landed, and at this release. About 6,000 commits separate them.

The changes a person would notice:

• Linux programs in windows. A Wayland bridge puts a program's window on the desktop, with a title bar and close, minimise and maximise buttons. KeePassXC, Telegram Desktop, foot and swayimg have drawn their windows on booted images. mpv and zathura are listed.
• Pseudo-terminals. Linux programs open /dev/ptmx and /dev/pts/N, so a terminal emulator can start its shell.
• Monero over Nym and Anyone. The Monero wallet syncs from its node through the mixnet or the onion network. A fresh wallet has refreshed in full on a KVM host.
• Installing Linux apps. An install checks every package against the signed index and fetches them one at a time over the chosen network. A failure names the package and the check that stopped it.
• Updates in place. A disk installed by 0.9.3 can be updated to a later release and keep its encrypted data volume.

The release notes name the file, commit or evidence directory behind each line. docs/release-evidence/0.9.3 indexes the evidence.

Figure 2. From a Marketplace listing to a window. Sources: docs/using/marketplace.md, docs/release/0.9.3-what-is-new.md.

31 Linux programs, each with its licence and its box in the catalogue (userland/capsule_market/linux-catalogue.json). Each is checked against a signed index before it installs.

The words in the last column are the box:

With a window:

In the terminal:

The Marketplace explains installing, and the Linux box what a box holds.

There are 67 driver capsules. Each runs in ring 3 with a claim on its own device, and DMA is confined by the IOMMU where the machine has one in service.

Which of these have run on real hardware, and which have run only in their host model, is set out in the 0.9.3 hardware notes. A driver whose device is missing leaves at once, and one whose device fails gives up after a few seconds.

• The kernel and every capsule carry a STARK proof that their measurement belongs to one policy root, and the boot refuses an image whose proof does not verify.
• Lean 4 holds 1,503 theorems about isolation, capabilities, the spawn path, page-table permissions, the attestation binding, the anti-rollback floor and the wipe at power off, with no sorry in any Lean tree. 115 Kani harnesses under userland/ and 222 proof crates run against the shipped source. These are the figures in verification/evidence/EVIDENCE.json; other counting rules give slightly higher numbers.
• The build is reproducible: make ends with a receipt of every artifact by sha256, and REPRODUCED when the artifacts match the committed receipts/<profile>.json.
• 57 evidence directories sit under docs/release-evidence/0.9.3, each naming the boot or test behind a line of the release notes.

NØNOS does not claim functional correctness of the whole kernel. The proved surface is what may run, what it may reach, and what survives a power cut. The proof suites says what each one guarantees, and verification/MAP.md ties each property to the source it constrains.

The driver classes are in Drivers. The machines they have run on, and the ones they have only been modelled for, are in the 0.9.3 hardware notes.

You need Nix with flakes turned on (https://nixos.org/download) and nothing else. On Linux and on a Mac with Apple silicon:

make # the kernel, every capsule, the Linux userland and the loader make check # every proof crate and every static check

On Windows, run the same two commands inside WSL2, or open the repository in its devcontainer (.devcontainer/), which has Nix already.

The toolchain, every crate and every C source are pinned by hash, and the build runs offline in Nix's sandbox. make ends with a receipt: every artifact by sha256, the toolchain and every pinned input, the kernel's own bytes held to the profile's promises, and REPRODUCED when the artifacts are byte for byte the ones in the committed receipts/<profile>.json. Those artifacts are unsigned, and no build ever needs a key. Enrolling and signing take the release keys, which are not in the tree:

make seal # enroll, sign and pack: needs the keys make boot # boot the sealed image under QEMU, with a TPM make boot-install # beside a blank disk, to try the installer make usb DISK=/dev/sdX # write it to a stick, after typing the path again

A build is one of the profiles below, set in nonos.toml or as PROFILE=airgapped make:

A release image is built hardened. docs/build is the step by step guide, from installing Nix on each platform to an installed disk. Build and verify is the whole flow, tools/nix/README.md the build in one page, and CONTRIBUTING.md the way in.

The release notes say what works, what does not, and how each line was shown:

• Known issues: a Linux app's home lives in memory and is gone at power off, creating a wallet on a machine with no TPM makes the keyring restart, SimpleX's desktop window is not in this release, and some programs listed in the Marketplace have not been booted.
• Security limits: on a machine whose firmware left VT-d or AMD-Vi off, a Standard boot goes on with device DMA unconfined and says so on its [IOMMU] line.
• Supported hardware: what has run on real silicon and what has run only in its host model.
• Upgrade notes: moving an installed system to 0.9.3.

Design work happens at discord.gg/nonos.

AGPL-3.0-or-later. Redistributable device firmware is not part of the source and carries its own terms.