The operatingsystem that proveswhat it runs.

Privacy

Traffic leaves
through a mixnet.

The network client is a real Nym client: five hops, Sphinx packets with a fresh key agreement at every hop, reply blocks. This release the shipped client held 128 nodes of the active set, built a four-hop route home, and fetched a real HTTPS page through it. There is no telemetry anywhere in the tree, and the shipped image carries no owner identity.

• 128 nodes held by the shipped client
• 4 hops home, measured
• 0 phone-home paths

Touchdown

A real machine.
Every piece of it accounted for.

This is a computer, and this is where NØNOS lives. The kernel is verified twice before it boots, the TPM measures the boot, and every driver, every window, every socket runs as a capsule that passed the gate.

Inside the processor

No process exists
until it has passed.

Everything that is not the kernel is a capsule: drivers, the network stack, the desktop, the browser, the wallet. There is no privileged tier. Each one is refused, not warned, at the first check it fails.

Authority

Every program announces
what it was given.

At spawn, on every boot, the kernel states which authority it actually granted to each program and who vouched for it. No mainstream operating system shows you that. What was never granted does not exist for that program, and there is nothing to escalate into.

Eleven checks

Certificate, anchor,
namespace, ceiling.

The certificate is decoded and verified against the trust anchor baked into the kernel, under the production policy, inside its validity window. The manifest is bound to it. A capsule cannot claim a namespace its certificate does not cover, or request more than the certificate allows.

Eleven checks

Two signatures,
one of them post-quantum.

Ed25519 and ML-DSA-65, both required, over the signed region. Then the manifest's payload hash must equal the hash of the actual ELF. Then the target triple. A capsule cannot register an endpoint its signed manifest does not declare.

Eleven checks

Then the proof.
Then, and only then, a PID.

Authority granted is what was requested, intersected with what was signed. Last, a transparent post-quantum proof of the binary itself. A missing or failing proof is one of exactly four refusals, and no process is created.

Refusal

The pipeline has refused
its own authors.

During the 0.9.2 cycle a stale dependency caused one capsule to rebuild in the middle of the signing pass. The re-verify step caught it by name and stopped before the ledger was stamped. Not a hypothetical. It happened, to us.

Nothing to sign with

Production builds
hold no keys.

A production build verifies the committed trust set and performs zero signing operations: 87 verifications, no signatures. The shipped image carries no device identity either. Its baked root authorizes nothing, and every binding proof against it is refused by design.

Proof

Counted honestly.

Machine-checked theorems about specific properties of specific code: capability bit semantics, context layout, parsers, crypto paths. Not a proof of functional correctness in the seL4 sense, and we do not claim that.

• 1,151 theorems and lemmas
• 165 Lean files
• 99 Kani harnesses
• 0 sorry in proofs

Verify it yourself

Eighty-eight proofs,
and the verifier is ours.

Every release ships the proof artifacts for the kernel and all eighty-seven capsules. The verifier that checks them in your browser is the operating system's own attestation crate compiled to WebAssembly, not a re-implementation, and its own test asserts that it refuses a tampered artifact.

• 88 attested artifacts per release
• 87 verifications in every production build

Attestation

The kernel proves itself
before the jump.

The bootloader verifies the kernel with two independent signatures, one of them post-quantum, then checks the kernel's own proof against a root baked into the bootloader itself. No trusted setup. The verifier that does this is the same code you can run in your browser.

The machine

Down to the silicon.

The TPM is spoken to directly and its floor only rises. Every entry into the kernel is hand-written assembly, one file per concern, so a reviewer can read the most sensitive instructions in the system without expanding a macro. Storage, USB, display and wireless run as capsules, and five families are proven on real hardware.

Software

Unmodified crates.io code,
running as attested capsules.

ripgrep, tokio, sd, grex, tokei and more compile for the NØNOS target and install behind the same gate as everything else. These are not ports. A full network stack as capsules, a browser fetching HTTPS through a four-hop mixnet route, nineteen driver capsules, five families proven on real silicon.

NOX Shield

Private transfers,
settled on Ethereum.

Private transfers and anonymous swaps that settle on Ethereum L1 under a transparent, post-quantum STARK with no trusted setup. Value conservation, ownership and double-spend prevention are each bound in the circuit, and every binding has a forgery in the test suite that proves it fires. Settlement is split across transactions because a single one would cost more gas than a block allows.

One thing is not done: the production proof vector still carries a stand-in rather than the live circuit, so today's published artifacts attest structure, not notes. The re-emit from the live circuit is scheduled for the first half of October.

Limits

What is not done,
in our own words.

The installer verifies but does not yet write to disk. Every shipped profile runs a single CPU. Real-hardware driver coverage is five families. aarch64 compiles and boots but is not a signed target. Performance numbers land in 0.9.3.

Public

Nothing runs on our servers
that you cannot run on yours.

Kernel, proofs, signing tools, documentation and the staking stack, all AGPL, all on GitHub. Eighty-eight proof artifacts ship with every release and the verifier is the operating system's own crate compiled to WebAssembly.

• 259,732 lines of kernel Rust
• 63 syscalls
• 88 attested artifacts