The next six releases.

Concurrency

1. Lost wake. A task decides to sleep while another core wakes it. The wake generation table is the existing defence and the model proves it over every interleaving rather than over the ones we thought of.
2. Reply misdelivery. A reply lands on the wrong caller when two callers on two cores are outstanding at once. This is the same shape as the correlation bug already fixed once on a single core, which is the reason it is first in the list rather than last.
3. Shootdown against unmap. One core invalidates while another unmaps the same range. Ordering of the invalidation, the page table write and the IPI acknowledgement is the whole problem, and it is stated as an invariant the model checks rather than as care taken while writing it.
4. Steal against exit. Work stealing picks up a task that is concurrently exiting. Bounded by making the queue's ownership transfer the only place a task changes cores.
5. Per-CPU aliasing. Any read of per-CPU state from the wrong core. Mechanically checkable, and checked mechanically, because this is the class that hides for months and then presents as a hardware fault on one machine.

The four-core hang currently in bring-up is expected to be class 1 or 5 and the models say which before anyone attaches a debugger. That is the difference between a schedule and a hope.

Isolation

Persistence

What is missing is the two calls that open it. Nothing in the kernel formats or mounts the volume, so /data resolves against a volume that was never mounted and everything a person writes lives in a ramfs that dies with the machine. This is precisely the pattern this project says it does not ship, written but unreachable from a running system, and it is listed here as unfinished rather than counted as a filesystem.

Then crash consistency, proved rather than asserted. Power cut at every commit point in a loop, remount, and the volume must come back at the old state or the new one and never at an invented one in between. A filesystem that has not been killed a few thousand times is a filesystem whose behaviour under power loss is unknown.

Then separation. The data capability grants a capsule its own subtree. The editor cannot read the wallet's files because it was never granted them, which is the same sentence as everywhere else in this system.

Power, and the firmware conversation

It is not enough for a laptop. Shutdown refuses, and the source says why: entering S5 means evaluating the _S5 object to get the sleep type values, which needs an interpreter. Sleep refuses for the same reason. The battery syscall returns a fixed hundred percent with a comment marking it as a placeholder until a real driver exists. Thermal is not read at all. Reboot works, because reboot is a register write the FADT hands you and needs no interpreter.

So four separate user-visible gaps are one missing component. One thing to build, built once, and four rows of the day table turn over together.

And it is firmware bytecode running inside an operating system whose entire argument is that nothing runs unverified. So it is bounded in every dimension that can run away, it refuses instead of guessing, it does not get kernel authority it does not need, and the firmware's opinion is treated as input rather than instruction.

The census ships in v0.9.3 for this reason among others. By the time the evaluator starts, the corpus already exists.

The work, in five phases, each with a number that moves.

1. Load and namespace. Walk the tables, build the namespace, resolve scopes and aliases, execute nothing. Signal: percentage of corpus tables that load with a complete namespace. Target 100, because a table that will not even load is a parser defect and not a firmware quirk.
2. Pure evaluation. Integers of both widths, buffers, packages, control flow, method invocation, locals and arguments. Validated by evaluating objects with no side effects, _STA and _CRS and _HID, across the whole corpus and comparing against what the existing bounded extractor already recovers on the machines it supports. Signal: percentage of corpus methods that evaluate without hitting an unimplemented opcode. The opcode set is finite and the burn-down is literally a checklist.
3. Operation regions. SystemIO and SystemMemory first, embedded controller after. This is where evaluation stops being pure and starts touching the machine, so it is gated: region access is allowed only from the evaluator, only to ranges the tables declare, and refused otherwise. Signal: corpus replay with regions mocked, then a single named machine with regions live.
4. Power. ACPI enable through SMI_CMD, _S5 evaluated, PM1 programmed. Signal: the machine turns off. There is no partial credit on this one.
5. Devices. _BIF and _BST for the battery, thermal zones and the passive trip point. Signal: a battery reading that tracks a discharge curve, and a throttle under sustained load.

Phases 1 and 2 are the bulk of it and both are measurable weekly against a corpus that already exists. Phases 3 through 5 are small once the evaluator is correct, which is the whole reason the order is this way round.

The installer

1. Surveys the machine through the hardware broker.
2. Reads the install set over the ramfs wire protocol, bounds-checking every length, offset and handle the server returns, because the file server is outside the installer's trust line.
3. Verifies each capsule's four artifacts through the same chain the spawn gate uses, printing the granted capability mask beside each verdict.

One verification failure ends the ritual. No path installs less and reports success.

The gap, and what each piece needs.

Step 4, mint the machine root. Needs the local-build root service exposed to capsules behind a physical-presence consent step, so a root is only minted by someone at the machine rather than by anything that can reach an IPC endpoint.

Step 5, write the boot partition. Needs two pieces, both specified and neither built.

Per-device driver instancing: the target disk must be served by its own driver instance, so the live medium is unreachable by construction. A region check is not an isolation boundary, and the store the boot chain trusts sits on that medium.

The write-authority ACL: the block driver answers mutating operations for the kernel client alone today. The installer earns that authority through the attested caller identity the kernel records at spawn, checked on every request and never cached, because a cached verdict outlives the installer's exit and would follow its pid to whatever runs next.

Step 6, enroll the composed system, so the machine attests as itself.

Step 7, the receipt: enrolled root, measurement set, slot labels. The numbers an owner writes down and later checks on the public page, closing the loop from a machine in a room to a verification anyone can repeat.

Drivers and hardware coverage

The system, five parts.

Attested census. Any live boot can run a per-driver census: probe, initialise, link, refuse, with reasons. One consent screen produces a signed report scrubbed to device identifiers and verdicts. No serials, no identity. QR rendering means the machine whose network driver did not come up, the one we most need to hear from, can still report.

The public matrix. Reports feed a hardware page beside the verify page. Rows are cryptographically checkable. It tells us what to fix by real population and tells a stranger whether their laptop works before they download anything.

Trace conformance. Every real-hardware session records the register and MMIO conversation. Traces become drop-in files CI replays against every driver change, along with hostile mutations. One afternoon with one borrowed laptop becomes a permanent regression asset that outlives the laptop. This is how the RTL8821CE work was proven off-silicon.

Variety without silicon. A QEMU device sweep across storage controllers, NICs, USB controllers, PCI topologies and core counts, plus bare-metal cloud runners for real Intel and AMD variety, rented by the hour.

The volunteer farm. A contributor with a remote-boot setup attaches a machine as a nightly target. They keep the machine, the matrix gets an attested report from hardware we have never touched, and nobody has to trust the report because it proves itself.

1. Parse the VBT to learn which display outputs this board actually has, since the hardware exposes far more than any given laptop wires up.
2. Read the EDID over the AUX channel, which is the first step with an observable: a panel's real mode list, printed.
3. Program the clock, then the pipe, transcoder and DDI in the order the manual specifies. Every step reads back, because a display pipeline that is programmed but not verified fails as a black screen with no information in it.
4. Page flip and vblank, so the compositor stops tearing.
5. 2D acceleration on the blitter, last, because a correct slow screen beats a fast broken one.

The network, and the anonymity we actually have

The client holds the whole active set. The directory endpoints answer with the rewarded set rather than every bonded node, currently 60 mix, 180 entry and 179 exit, and a node is 76 bytes on the wire, so all of it is under 40 KB and there is nothing to ration. Hop selection reads four bytes of the route seed through a multiply-shift reduction, which is uniform over the candidates to within one draw and reaches every candidate however long the list is.

The marketplace

The desktop scans /pkgs each tick, lists installable packages, and raises a consent screen showing requested capabilities by name before approve commits anything. It never hides a capability to look friendlier. The terminal has the same power in text.

First package through that path: a QR generator built from an unmodified crates.io crate, signed, verified, consented to, installed.

Running the software people already have

Three ladders, in the order they become possible, each honest about what it gives you.

Why an operating system is the missing layer

Hardware wallets exist because operating systems cannot be trusted. So does the seed phrase written on paper, the blind-signing screen on a second device, and the habit of keeping a separate laptop for anything that holds value. Every one of those is a workaround for a single fact: you do not know what is running on the machine in front of you.

Web3 has spent a decade engineering around that fact rather than at it. The keys moved off the computer because the computer was the problem. It worked, and it is why using a hardware wallet still feels like using a hardware wallet.

NONOS goes at the premise. If every byte that runs was verified before it ran, and the signing key is sealed to the measurement of the system that runs it, then the machine you are already using is the signer. Not a second device you carry, not a phrase in a drawer. The computer, because the computer can prove what it is.

That claim is not finished, and the honest position is written into the sections below. The custody path is real and the sealing that makes the claim true lands in v0.9.5. Until then this is an argument with the mechanism half built, and it is described that way.

The wallet

Payments, and why they are a capability

Behind it sit three crates that are pure logic and therefore provable on a host, which is where they are proven. nonos_nox_receipt accepts a chain receipt only when it shows a successful transaction carrying an ERC20 transfer from the buyer to the treasury, emitted by the NOX token, for at least the price. It reads only the fields the decision needs and never allocates, so a truncated or hostile receipt fails closed instead of reading as a payment. nonos_nox_broker prices the tool, checks the receipt, refuses a transaction already redeemed, and returns exactly the grant that was paid for. It never signs: the capsule holds the key. nonos_nox_license verifies the entitlement, with signature checking injected through a trait so the same code runs against the kernel's ed25519 in a capsule and against a host signer in tests.

Thirty-three tests and nine Kani proofs across the three.

That is also the answer to agentic payments, and it is the opposite of how the rest of the industry is approaching them. Handing an autonomous process a key and hoping the sandbox holds is a trust model. Requiring that the process spending money is a binary whose hash was enrolled, that declared spend authority in a signed manifest, and that a spawn gate admitted after checking eleven things, is a proof. The keyring already carries the x402 rail in its wallet rail registry, marked as requiring configuration, which is the correct state for something that must not work by accident.

The SDK, and the developer path

marketplace_abi carries the index wire form as a length-prefixed binary codec against a canonical schema, deliberately not JSON, because a marketplace index arrives as a signed blob and a tight parser keeps the userland attack surface narrow.

Micro fees, and where they can actually settle

The marketplace wants per-use pricing. A tool that costs a fraction of a cent per invocation is the natural shape for a capsule that does one thing, and the licence and broker crates already implement exactly that: one use per price paid, replay refused, grant issued only against a confirmed payment.

That shape does not settle on Ethereum mainnet, and saying otherwise would be the first dishonest sentence in this document. A per-use fee worth a fraction of a cent cannot carry a mainnet transaction. The mechanism is right and the settlement layer is the open question.

Three answers exist and each has a real cost. A rollup, where fees are small enough for per-use settlement and the receipt verification we already have works essentially unchanged, at the price of a bridge and a second place where value lives. Payment channels, where a buyer opens once and settles a batch, cheapest per use and heaviest in state to manage. Batched settlement, where the broker aggregates and settles periodically on mainnet, simplest to build and the one that requires trusting the broker between settlements, which is the thing this project exists to avoid.

The answer is a decision rather than a discovery, it is recorded in the open decisions below, and it is answered before entitlements gate spawning rather than after. Whatever wins, the anchor stays Ethereum and the receipt stays something anyone can check.

What you see is what you sign

This is the oldest unsolved problem in crypto user experience and it is not a wallet problem. You approve a transaction because a window told you what it does. On a general purpose operating system, nothing establishes that the window is the wallet's, that the text in it matches the bytes being signed, or that a screenshot of a wallet is not simply a screenshot of a wallet. Hardware wallets exist to move the confirmation onto a screen the host cannot draw on, and the second screen is small and shows you an address.

NONOS has the pieces to close this properly, which is not a claim that it is closed. The compositor is an attested capsule with its own proofs. The wallet is an attested capsule. Capability bits are already shown to a person before an install, so a consent surface owned by the system rather than by the application is an existing pattern here rather than a new idea. What is missing is the binding: a confirmation surface the requesting application cannot draw, cannot read, and cannot dismiss, that displays the decoded transaction and returns a signature only for the bytes it displayed.

Done properly it means the confirmation is a trusted path from the capsule that decodes the transaction to the pixels the owner reads, on the machine they are already using, with the whole chain attested. That is the thing the second device was invented to approximate.

The chain side, and why Ethereum

Eight contracts are live on Ethereum mainnet under a three-of-five Safe, and the Rust claim path settles against the deployed pool rather than a local fixture. The off-chain rail has a frozen leaf format and five tools behind a single make target, which is what keeps the format from drifting under the thing that depends on it.

We build on Ethereum and we are not going to launch a chain. The reason is not diplomacy. A new chain would mean asking people to trust a new validator set in a document whose entire argument is that they should not have to trust anyone, and it would let us grade our own homework on the one part of the stack that already has adversaries paying attention. The settlement layer is the part of this system we most want to be somebody else's problem, audited by more people than we will ever have.

So Ethereum is the anchor and the verifier lives there. Shield's proofs verify in deployed bytecode. Payments are ERC20 transfers anyone can check. Where fees make mainnet the wrong venue, the answer is a layer above it that settles down to it, never a chain beside it.

The interesting claim was never on the chain anyway. It is that the machine holding the key can prove what it is, and every part of the stack above exists to make that provable rather than asserted.

What this makes possible, which we are not building

Not scheduled, not promised, not counted anywhere in this document. They are here because the primitive is real and somebody should build them, and because a roadmap that only lists our own work is a smaller document than it needs to be.

The primitive is one sentence: a machine that can prove which software it is running, holding a key that only exists while that proof holds. Trusted execution environments have promised this for a decade from inside vendor silicon whose failures are somebody else's disclosure timeline. This version is open, reproducible from a public commit, signed twice, and attested by a STARK anyone can verify.

We are building the primitive and the OS around it. If a year from now somebody has built two of these on top, that is a better outcome than us having built one of them badly.

Where it stands

The 2-in-2-out join-split circuit is built and gate-green. It proves note commitment under the deployed 32-round hash, membership in a depth-32 pool tree, that spent notes are proven notes, value conservation bound to committed limbs so neither mint nor burn is expressible, and ownership plus double-spend through keys derived from one witnessed spending key. Fourteen bindings each carry a forgery proving that binding fires, and a meta-test fails if a binding is added without one. The forgery suite runs against a minimal instance so it gates every change, with the full deployed depth as a release gate, because a minimal stand-in is only valid while it provably tracks the real one.

The key hierarchy is frozen and dual-reproduced. The recursion hash runs at the deployed round count.

On settlement, the split-transaction verifier is built and gated against the real L1 vector: accept-real plus the reject suite, with begin measured at 32.7M gas against a 36M block ceiling. Single-transaction verification at 128-bit security was measured at 121M gas and is therefore impossible on L1, which is why settlement is split across transactions with the first one binding every challenge and query index so later chunks cannot be crafted independently.

The pool contract carries a fail-closed beta gate: allowlist, per-asset caps, and refunds that always return to the recorded depositor, so governance can push funds to that person and to nobody else.

The memory wall, and why it stopped being the blocker

Those last figures are projections from a shape nobody has yet built at full scale, and this document does not treat them as results. The first production bake receipt is what converts them, and until it exists the re-emit below is gated on that receipt and on nothing else.

Milestones

Gauntlet and audit preparation.

Public deposits.

Decisions recorded