Wolkie Atto-Kernel

A formally verified, deterministic atto-kernel that runs WebAssembly on the metal.

Wolkie is a research kernel for x86-64. It boots directly from UEFI, owns the paging structures, the interrupt path and every device it drives, and executes user programs exclusively as sandboxed WebAssembly modules. Authority is granted per run as a capability mask, work is metered in fuel, and the security-critical decisions are written as contracts in Ada/SPARK and checked with GNATprove. The remaining behaviour is either modelled (TLA+, Alloy) or measured by a gate with a stored run.

The kernel is a research prototype. It is not a production operating system, it does not load ELF binaries, and it does not offer a POSIX interface. Section Hard limits states in numbers what a program has to fit today.

Generated by ./scripts/tools/readme_at_a_glance.sh from the tree on disk - do not edit by hand.

At a glance	Count	Where it comes from
WebAssembly modules in the image	23	rows in apps/apps.manifest
Console commands	27	Command_is arms in arbiter_main.adb, as a set
Boot gates (one crossing each)	26	scripts/run_*.sh
Host checks	23	scripts/check_*.sh
Rust subsystem crates	9	directories under src/rust/
Ada/SPARK units (arbiter)	31	src/ada_spark/core/main/arbiter_*.ads
Design diagrams	8	design/*.puml

Build and validate: ./scripts/test_all.sh, then ./scripts/prove/prove_spark.sh, then ./scripts/build_all.sh - three commands, no arguments, each honest about what it could not measure. A boot gate is one command too: ./scripts/gates/run_boot_root.sh.

---

Contents

1. Overview
2. Strengths and limits
3. Architecture and portability
4. Boot: from firmware to the shell
5. Modules, drivers and the HAL
6. Dependencies and references
7. Security, tests and enforcement
8. License
9. Repository layout
10. Terms used in this document
11. Hardware requirements

---

1. Overview

A kernel answers five questions: which address space is active, which code may run privileged, what a program may touch, what a program costs, and what happens when it misbehaves. Wolkie answers them with five decisions.

Decision	Consequence in this tree
User code is WebAssembly, not machine code.	A program is a module executed by a bounded interpreter. It cannot issue a privileged instruction, map memory or reach a device; it can only call the host functions its run exposes.
Every space has its own page-table root.	The kernel maps itself and the user program through separate roots (page-table isolation, KPTI). A user root carries the user program and a short, explicitly named list of supervisor pages the CPU itself needs.
Authority is a capability, not a name.	A run starts with a rights mask; every object a module opens carries a token the capability broker mints and can revoke. The right is checked before the object is interpreted.
Work is metered.	The interpreter charges fuel per executed instruction. A Tier-1 run that exhausts its budget is trapped and rolled back; a Tier-2 run is parked with no budget held and receives a fixed quota per event.
State is published as immutable, hashed records.	Address spaces publish state through the State Update Hub (SUH); content is addressed by hash in T-CAS. A rollback selects an earlier epoch root instead of replaying an undo log.

What that design buys is a kernel whose critical rules are small enough to be proved, and a user space that cannot escape by running native code. What it costs is a module profile a program has to fit; both sides are stated in Section 2.

---

2. Strengths and limits

What holds, and on what evidence

The project separates three kinds of evidence and always says which claim rests on which. A fourth kind - "it works" - is not accepted anywhere in this tree.

Property	Mechanism	Evidence class
Policy and lifecycle decisions	Ada/SPARK contracts: preconditions, postconditions, loop and type invariants, abstract state with a proved refinement	proved (GNATprove)
One live capability handle per space, monotonically rising ids	arbiter_handle_ledger, plus a bounded-model-checking harness	proved and model-checked (Kani, optional)
Address-space isolation and page-table ownership	src/rust/mmu, held against the Alloy model Wolkie_MMU.als	modelled (Alloy 6)
Epoch publication, rollback, park and resume	arbiter_hasf, arbiter_park_lifecycle, the TLA⁺ models for epochs and fuel	modelled (TLA⁺/TLC)
Interpreter conformance (instruction set, traps, bounds)	crate tests over hand-written and compiler-emitted bytecode	measured
The C-ABI crossings	tests/rust-abi/, black-box	measured
Boot paths (default root, MMU probes, ring 3, CPL3 process, WASI 0.3 wait, NDN, CMR)	one gate per path, each with a stored run	measured
Determinism of a result across nodes	canonical NaN normalisation, integer-only rounding, no host math library	by construction, checked by tests

Two qualifications belong to that table. A proof is a statement about the specified behaviour: if a contract is wrong, the proof says nothing about the world. And the statements about hardware behaviour are models of it - this document claims no silicon enforcement where only a software model exists (IOMMU, cache-way locking, mesh replication).

Hard limits: why they exist, and what lifting them would cost

These are the structural bounds of the current profile. Each is a constant in the tree rather than a tuning parameter, and each exists for a reason that can be named. "Cost" is what removing it would take: memory, a second execution model, or proof obligations.

Limit	Value	Why the bound is there	What lifting it would cost
Module size	at most 1 MiB	the module is validated in full before its first instruction, and it is embedded in the boot image	a streaming two-pass validator and a loader that can page a module in; the image grows by the module's bytes
Basic regions per function body	512 per call level	the region table is a slice the caller reserves, not engine state, so the engine keeps a fixed size	the reservation is per call level, so the slice grows linearly with the depth bound; validation cost grows with it
Call depth	2 frames (3 levels)	each level costs a native interpreter frame plus its own region slice; the engine does not recurse natively	a frame-model change: an explicit frame array with its own discipline. This is the bound most likely to block a real-world port, and the one a std-linked guest meets first
Block nesting per body	24 levels	the label arrays are static state, so nesting becomes table entries instead of native recursion	more static state (three label arrays) and a re-measured splitter
Guest functions / table elements / globals / locals / operand values	256 / 512 / 8 / 64 / 128	fixed tables in a no_std engine with no allocator	direct static growth; the per-run reservation grows with the maxima
Linear memory	256 pages (16 MiB) declared by the module; the console hands a run 8 pages per half	a run's pages are the caller's reservation, and a parked run needs a second copy as the rollback image	double the per-run reservation, plus a memory.grow contract the engine does not have
Host imports	30 per module	the binding table is fixed and the binding index is a masked byte	a wider index encoding, a larger table, and a second byte in every call site
Open descriptors	8 per instance	one resource table per instance, indexed by handle	a larger table per instance - that is, per parked instance as well
Integer remainder (i32.rem_*, i64.rem_*)	not implemented	the arm set is a deliberate subset; a rem is refused at load rather than half-executed	one engine arm per form plus its conformance tests - the cheapest entry in this table, and an open engine item
NDN forwarder tables	Pending Interest Table 32, Forwarding Information Base 16, Content Store 64 (LRU)	heapless collections and no allocator at all: a growable heap would end deterministic execution	static memory per instance, and an eviction policy that stays a pure function of the arrival order
UDP sockets	4	one static socket table in drivers::net, each slot a fixed ring	memory per slot and a re-measured queue ladder
Sealed seed slots	7 spaces	the seeds live in the reserved secure window of the image	a larger secure window, and the derivation and provisioning path re-proved for it
Network layer	L1 only: Ethernet, ARP, IPv4, ICMP, UDP	a record layer (TLS/QUIC) is a second state machine this profile does not carry; above UDP the guest speaks NDN	TCP + TLS 1.3 + QUIC/HTTP/3 is a stream subsystem, not a bound - it is excluded by decision, not pending
Concurrency inside a module	none: no threads, no atomics, no shared memory	the interpreter runs one instance to completion or parks it; isolation is per space	a concurrent execution model, which contradicts the deterministic-hash design
Modules per run	one, with one exported _start	one engine instance, one run at a time, no nesting	dynamic linking and a second execution model inside one engine

Two consequences follow directly, and they are the practical reading of the table. First, a compiler emits a basic-region boundary for every call, end, else and loop, so the profile suits small purpose-built modules and compact compiled guests; a program with a deep call graph meets the depth bound before it meets any other. Second, a program that links a general-purpose language runtime is out of scope by decision: a std-linked Rust binary or a C program with a full libc nests deeper than the profile allows before its own first instruction runs.

What fits today: a console utility that takes a path and prints what it reads; a filter that consumes one line and answers it; a parser or calculator that evaluates one element of a document; a probe that reports the run's own state; an integer-only routine - a checksum, a hash, a fixed-point calculation - that finishes inside its budget. The modules in apps/wasm/ are exactly that class, and they are the reference implementation of the profile.

---

3. Architecture and portability

The layers

Wolkie is written in four languages because each component class has exactly one language that can carry its guarantee. The table is the architecture in one screen; the crossings between the rows are described after it.

Layer	Written in	What it owns	What it may not do
User space (apps/wasm/, src/rust/ndn_guest/)	WebAssembly	the console commands, the process payloads, the NDN forwarder	execute native instructions, start a process, stop the machine, reach a device
WASM runtime (src/wasm/)	Rust	loading and validating a module, interpreting it, metering fuel, binding imports by name, the resource table, a parked instance's continuation, answering a refusal in the caller's error space	grant authority; it asks the subsystems through their C-ABI gateways
Subsystem crates (src/rust/)	Rust	paging and address spaces (mmu), content-addressed storage and the VFS (storage), capability broker, state fabric and commitments (arbiter_shim), device queues and the NVMe/virtio-net models (drivers), root replication and post-quantum exchange (mesh), the NDN wire format (ndn)	decide policy for a space, or execute privileged instructions
Arbiter and policy (src/ada_spark/core/main/)	Ada/SPARK	boot order, per-core arbitration, the console shell, process lifecycle, the capability-handle ledger, the policy contracts	import Rust directly; every crossing is a C-ABI gateway
Hardware abstraction (src/ada_spark/core/boot/arch/x86_64/)	Ada/SPARK protocols, C and assembly stubs	the only privileged layer: page-table roots, interrupt tables, timers, serial console, CPU bring-up, firmware calls	let a stub make a decision; the protocol decides, the stub executes one instruction
Firmware and machine	UEFI, x86-64, QEMU/KVM	boot services, interrupt controller, devices, the CPU	carry any Wolkie rule

The rules that hold between the layers. They are conventions a change is measured against, and the first is enforced mechanically.

1. The C ABI is the only crossing. Ada/SPARK never imports Rust, and Rust never imports Ada. Both sides speak the Windows x64 convention - arguments in RCX/RDX/R8/R9 plus 32 bytes of shadow space - through arch_* and vki_* gateways; scripts/checks/check_abi.sh refuses a direct import even when it links.
2. Every shared structure has one writer. Where two subsystems touch the same state, the lock is defined at the hardware abstraction boundary with a documented order, so ownership is a fact a reader can check rather than an assumption.
3. A module reads and computes; it does not orchestrate. It can list, read and parse, evaluate an expression handed to it, publish a state frame and present a capability. Starting another module or stopping the machine is the launcher's and the kernel's decision.
4. A refusal names its reason, and the documentation pairs every refusal with its acceptance. "It was rejected" is never evidence on its own - a mistyped address is rejected too.

Portability: what a port replaces, and what it keeps

The tree ships exactly one architecture, x86-64. The portability claim is about the shape of the boundary, and it is best stated as a split rather than a promise:

Region	What a port replaces	What a port keeps
Instruction primitives - rdmsr/wrmsr, CR3/INVLPG, lgdt/lidt/ltr, port I/O, rdtsc/lfence, sti/hlt/pause, xsetbv	the one-line C or assembly stub behind the arch_* symbol	the Ada/SPARK protocol that calls it, its contracts, and the policy that decides when it is called
Page tables, interrupt controller, timers, serial, CPU bring-up, firmware entry	the HAL implementation for the new platform	every proof above the HAL, the arbiter, the subsystem crates, the interpreter and the module profile
Devices (NVMe, virtio-net)	the device model in drivers plus its arch_* gateways	the queue protocol, the capability checks, the refusal codes and their tests

That split is the result of a deliberate migration: the decision moved into Ada/SPARK with contracts, the instruction stayed a stub. A new architecture therefore owes a stub set, a boot entry path and a device model - not a second kernel. The record of that migration, region by region with the run behind each slice, is in docs/ROUNDS.md.

Portability of results is a second, independent property, and it is why the interpreter normalises what hardware disagrees about: a NaN an operation produces is the canonical bit pattern, rounding and the square root are computed over the bits with integer arithmetic, and no host math library is linked. Two machines that ran one module therefore hash the same bytes - which is the precondition for the mesh below.

Network and mesh

The wire exists as far as datagrams need it, and L1 is its hard ceiling. The kernel drives virtio-net in the HAL, takes one DHCP lease, and speaks Ethernet, ARP, IPv4, ICMP and UDP; wasi:sockets' UDP half is served by that same stack, so a module binds a port, sends a datagram and reads the answer. TCP, TLS 1.3/AEAD record layers and with them QUIC and HTTP/3 are excluded from kernel and guest space by decision: a record layer is a second state machine this no_std, call-depth-bounded, proof-carrying profile does not carry.

Above L1 the guest is data-centric instead of connection-centric: Named Data Networking over UDP - content-named Interest and Data packets, in-network reuse through a bounded Content Store, and provenance from content signatures instead of a session handshake. It is built as two crates and one module:

• src/rust/ndn/ is the dependency-free Interest/Data codec, shared by the kernel and the guest.
• src/rust/ndn_guest/ is the forwarder: no_std, heapless, built for wasm32-unknown-unknown, with the three bounded tables named in Section 2.
• The module is embedded in the boot image like every other one and runs behind the console command ndn; the Causal Mesh Router's root advertisement sits one layer above it (cmr), and the module publishes its own census on that layer: the claim is signed with its own space's seed, so a peer can tell whose state it read - the node vouches for nothing it did not sign itself.

The forwarding rules see encoded packets - the module decodes what arrives, decides (Content Store, then the pending table, then the route) and encodes what leaves - so the same rules run under the host test suite and inside the boot image. The wire, the clock and the signature check are the host's, and the module sees them only through wolkie.*. A node's own claim is published by the host (mesh::gossip, signed with the arbiter's seed slot), never by a guest: a guest that could sign would be able to speak in the node's name.

resolve-addresses is retired rather than pending: with NDN the name is the address, so there is nothing to resolve and no second stack to resolve it with - and the canonical arm it held went to the guest's one-shot crypto.hash, because the surface has no free slot (all 64 are allocated). A module that still imports the old name binds nothing, and a call through it traps.

The comparison diagrams under design/ place this kernel beside a monolithic, a microkernel and a hybrid design along one subsystem per file (kernel_hw_comparison.puml, kernel_process_comparison.puml, kernel_memory_comparison.puml, kernel_filesystem_comparison.puml, kernel_network_comparison.puml, kernel_signals_comparison.puml). They are discussion material: their claims about the other three designs are textbook summaries, and only the Wolkie column is held to the measured evidence.

---

4. Boot: from firmware to the shell

Wolkie boots through UEFI and only through UEFI. There is no legacy BIOS path and no second-stage bootloader: the build produces a PE/COFF EFI application, packs it into a FAT ESP image, and everything from the firmware hand-over to the prompt runs in one image. The reason is not taste - UEFI hands over a 64-bit processor in long mode with a memory map and a system table, which the kernel needs anyway, and the firmware's calling convention (Windows x64) is the one this tree speaks everywhere. A BIOS path would need a real-mode transition, its own loader and a second ABI. The sequence below is the code path, in order.

Stage 0 - firmware loads the image

The UEFI firmware loads boot.efi as a UEFI application and transfers control to its entry point _start in the assembly wrapper. The wrapper saves the pointer to the system table (passed in RDX under the Windows x64 convention), aligns the stack to 16 bytes, reserves the 32 bytes of shadow space the convention requires, and calls prototype_main.

Stage 1 - the UEFI stub (uefi_main.c)

Still inside boot services, in this order:

1. Serial console. The HAL initialises COM1 (0x3F8). From here the log is the UART's - the firmware console is written to once more later, and then never again.
2. Keyboard queue. The input queue is initialised even when interrupt delivery is deferred, so the queue state at hand-over is deterministic.
3. Entropy. The boot locates the firmware's random-number protocol and probes RDRAND as the fallback. If neither exists, cryptographic key generation is refused and says so - the boot fails closed rather than inventing a seed.
4. Firmware facts. The ACPI RSDP is captured while the configuration tables are valid, and the image's own facts are recorded: where the firmware placed it, the relocation verdict, the memory-map cross-check, the text and data page counts, and whether the image touches the secure window.
5. The display surface. The GraphicsOutput framebuffer's geometry - base, size, width, height, stride and pixel format - is read here, because its address is only meaningful while the firmware's identity map is in force. The kernel keeps the geometry and hands it to user space: there is no font, no text composition and no UI in the kernel, and a machine without a framebuffer keeps the serial console as its terminal.
6. No boot-services allocation. The only one this path ever made - the three STREAM buffers the retired benchmark measured - left with the benchmark (TODOS.md item 28). Every buffer the kernel uses is static, so the boot path never calls AllocatePages and ExitBootServices is not waited on by an outstanding allocation.
7. ExitBootServices. With a retry for a memory map that grew between the two calls. It is the point of no return: ConOut, pool allocation and the firmware RNG are gone afterwards, and the RNG protocol pointer is dropped because its memory is no longer ours.

Stage 2 - the HAL brings the machine up (arch_enter_arbiter)

The boot entry point then hands over to the HAL, which owns the privileged part:

1. Bootstrap page tables. An identity map for the running image, so that code and data are reachable while the managed roots are built.
2. CPU tables. Global and interrupt descriptor tables and the task-state segment, the AP trampoline copied to its reserved physical page, the interrupt stack, and the timer.
3. Shared pages. The pages holding the descriptor tables and the TSS/interrupt stack are registered, not mapped: the manager maps exactly these into every user root, because an interrupt is delivered on the user root without a CR3 change.
4. Managed root. The MMU builds kernel space 0 in two phases - the template and trampoline page first, then the class-driven mapping of everything registered between the phases - and verifies the result. The seed stack's guard page is deliberately unmapped at the end of the run, and the kernel's own text is committed before and after the bring-up as a stability check.
5. The switch. CR3 is loaded with the manager root, so the kernel stops running on the bootstrap map; the stack is switched to the arbiter's own fixed-size stack, and the fact is printed before the first Ada frame exists.

Stage 3 - the Ada/SPARK arbiter starts

arbiter_main initialises the subsystems, seeds the capability broker from the platform random source (and prints whether it succeeded), brings the per-core arbiters online, enables the local APIC, brings the network device up and takes its DHCP lease, reads the ACPI MADT for the core inventory, commits the genesis intent vector, opens a short deterministic warm-up window, enables interrupt delivery, and reports how many cores reached the online state before entering the shell.

Stage 4 - the shell

The console is part of the arbiter, not a process. A line typed on the serial port is read by the tick and dispatched by name: the kernel answers a small set of commands itself (the ones that touch kernel state directly), and the rest are handed to the module launcher with a module id. The launcher - not the shell - owns the capability mask and the fuel budget for that module, so a command name cannot grant a right. A module's answer comes back as a State Update Hub document, and the shell prints the element the caller asked for. A Tier-2 module that waits is parked; the arbiter resumes it when the event it named arrives.

---

5. Modules, drivers and the HAL

5.1 The module profile

"Compatible with Wolkie" means fits this profile, not "compiles somewhere and runs". The profile is what the validator enforces at load time, before a single instruction executes.

Requirement	What Wolkie expects	Why
Target	wasm32, freestanding: no libc, no POSIX, no threads	the interpreter executes a defined subset; there is no C runtime behind it, and a guest brings the few routines it needs itself
Memory	one linear memory, as many pages as the module's own memory section declares; no memory.grow	the run's pages are the caller's reservation, and the module's section decides how much of it the guest may address
Link flags	--initial-memory=65536 --max-memory=65536, stack at the bottom (--stack-first -z stack-size=8192), --export=_start	compiler defaults put the stack above the first page and assume a growable memory
Allocator	export cabi_realloc only when the canonical WASI 0.3 names hand a list or record back	the canonical ABI lets the guest allocate the return area; the flat names need no allocator
Entry point	one exported _start, executed once per run	one engine instance, one run at a time, no nesting
Imports	at most 30, all from the profile's surface; an unknown name binds nothing and a call through it traps	a name grants exactly what it names; nothing is aliased onto another host function
Instruction set	integer and memory instructions, branches, call/call_indirect, globals, select, the six memory forms, and the complete f32/f64 set (arithmetic, twelve comparisons, rounding, sqrt, conversions including the eight saturating trunc_sat) - but no integer remainder	the engine's tables implement exactly this set; anything else is refused at load rather than half-executed
Structure	512 basic regions per body per call level, 24 nesting levels, 256 functions, 512 table elements, 8 globals, 64 locals, 128 operand values, call depth 2	fixed tables in a no_std engine; the region and frame reservations are supplied by the caller, not kept as engine state
I/O	streams and descriptors (fd_read, fd_write, path_open, poll_oneoff), and on the versioned names a future (subscribe, subscribe-duration, future.read)	a module has no ambient file system; the VFS resolves a path, the broker decides whether a descriptor may be used, and a wait is a park the arbiter owns
Authority	only the rights of its run	a call without its right traps and rolls the run back
Budget	a one-shot fuel budget (Tier 1) or a fixed quota per event (Tier 2)	a runaway module is impossible by construction

The reference for what a compiled guest looks like in this profile is the generated C guest under src/wasm/tests/fixtures/, which links the canonical adapter; how it is built is in docs/DEVELOPMENT.md -> "Prerequisites".

5.2 What a module can reach

The surface is one dispatcher with two faces: the profile's own wolkie.* names and the versioned interface names of WASI 0.3 (wasi:io/streams, wasi:io/poll, wasi:clocks/monotonic-clock, wasi:filesystem/types, wasi:cli/environment, and this tree's own wolkie:filesystem). The same arm answers both; the faces differ only in the error space a refusal is returned in. The flat names of wasi_snapshot_preview1 were the third face and retired on 2026-10-29: no module in the tree imports them, and an image written while they existed is refused rather than decoded without them.

Grouped by what a module wants to do:

• Write output: print, and fd_write on the console descriptors. A write is shortened when the document's bound fills, and the returned count says how much landed.
• Read input: fd_read on the console - the line that invoked the command, or the keystrokes a parked instance was woken for - and poll_oneoff to wait.
• Wait on a completion: on the versioned names, input-stream.subscribe and the clock's two subscriptions hand back a future, and future.read either answers at once or parks the instance until the arbiter delivers the event.
• Read files: the descriptor calls (path_open, fd_read, fd_seek, fd_close, fd_filestat_get, fd_readdir, path_filestat_get) when a module walks a directory or reads in pieces. Storage is read-oriented: a module reads and lists, it does not create or modify files. The console's own ls and cat commands - and the three wolkie.* names they used (ls, cat, cat_field) - retired with the four seeded files (TODOS.md item 13): they no longer bind, so a module that imports them is refused rather than served by an empty VFS. What is left of the read path is the descriptor surface above, over a VFS the image seeds with one probe path.
• Inspect itself: status (fuel, rights, root), suh_field to read one element of the run's document, suh_publish to publish one.
• Time and entropy: clock_time_get, clock_res_get, random_get - one platform source for both, so a nonce and a filled buffer cannot come from different pools.
• Store and fetch flat values: the key-value get/set over a small bounded namespace, behind the read and write rights. A key is a key, not a file.
• Hash data: hash, the one-shot BLAKE3 digest (32 bytes) that the census fold is built from. No right and no key
  • the guest passes bytes it already holds, and the answer is the digest the storage fabric commits with, so a root computed in a module is a root a peer can compare.
• Use a privilege: pqc_seal, pqc_attest, ipc_send_token, and crypto.sign, each behind its own right. crypto.sign reaches the kernel's sealed seed pool: the space comes from the host, the guest names only its handle, and the signature is produced on the signer's own stack.
• End or yield a run: proc_exit, sched_yield.

The complete, current list with the right each call needs and the gate that compares the names lives in design/architecture_detail.puml and docs/DEVELOPMENT.md. It is deliberately not duplicated here: a second copy of a list is a second thing to keep true.

5.3 Building a module: the touch-points

A module becomes a console command through seven touch-points, and skipping one shows up either as a red gate or as a command that answers "Unknown command". The order matters, because each step is checked by the next:

1. The source - a .wat under apps/wasm/, or a compiled module of the same profile.
2. The bytes - compiled at build time into the image; no loader, no path resolution at run time.
3. The module id - a case in the HAL's console launcher, which also owns the capability mask and the fuel budget of that module.
4. The command - a branch in the shell's dispatch that maps a name to that id.
5. The documentation lists - the shell's commands and the apps/ modules are compared with the code as sets by a gate, so a new command cannot be half-documented.
6. The host surface - only changes if the module needs a call the surface does not have. That is an engine change: a new arm with its right, its fuel rate and its test - not a documentation edit.
7. A boot run that types the command (see scripts/gates/run_boot_root.sh and its console variables), whose verdict line carries the command it typed, so the run says what it proved.

The .wat files are the source of the bytes: the build compiles them, and the generated header is build output, never tree content. src/wasm/wit/wolkie.wit is the contract the surface is written against - resources, streams, the error enumeration and the record shapes a canonical guest expects - and its generated C bindings are committed, regenerated by scripts/build/generate_wit_bindings.sh and held to the tree's constants by scripts/checks/check_wit_bindings.sh. The package is self-contained on purpose: it declares its own error enumeration and flags instead of importing wasi:io, because resolving those would make the generator reach a package registry over the network, and every artefact in this tree is reproducible offline.

5.4 Drivers and the HAL: the rule a new device follows

A driver is HAL code, not a crate. Device work lives in src/ada_spark/core/boot/arch/x86_64/ (C, plus assembly for stubs and the AP trampoline) and reaches the managers through arch_* gateways. The shape is fixed by the HAL migration and applies to every new region:

Part	Where it lives	Why there
The protocol - registers, states, refusals, ordering	Ada/SPARK in src/ada_spark/core/main/, with contracts	it is the part that carries a proof
The instruction - in/out, rdmsr, a ring descriptor write, a queue doorbell	a one-line C or assembly stub behind an arch_* symbol	it touches privileged state that only the HAL may touch
The manager - queues, leases, state, policy results	Rust (drivers), behind a C-ABI export	memory-safe model code with crate tests
The crossing	the C ABI, in Windows x64 form	the only allowed crossing between the layers

A new C-ABI export is one change, not several: gateway, header declaration, Rust export, host test under tests/rust-abi/, and the docs/DEVELOPMENT.md entry. scripts/tools/scaffold_abi.sh names the four touch-points and can verify an existing symbol; scripts/checks/check_abi.sh refuses a direct import across the boundary even when it links.

5.5 Running a module without booting

tools/wasm-runner executes a module on the host with the same interpreter the kernel embeds, with the same capability masks and a seeded VFS, which is how most of the surface is measured before a boot gate runs. A boot gate is what proves the crossing into the image: the same module, the same capability, the same interpreter, on the machine.

---

6. Dependencies and references

6.1 Toolchain

Development happens in a POSIX environment (Ubuntu or WSL2) because the automation is Bash. The table says which part of the tree needs which tool, and which of them are optional - an optional tool's absence produces a skip, never a pass. The exact package names are in docs/DEVELOPMENT.md -> "Prerequisites".

Tool	Needed by	Optional
Rust (stable, cargo)	every crate, the interpreter, the UEFI bundle, the host tools	no
GNAT 14 + gprbuild, compiled at Ada 2022	the arbiter and the HAL protocols	no
wat2wasm (wabt)	compiling apps/wasm/*.wat into the bytes the image embeds	no
Bash, git, core utilities	the build, test and gate scripts	no
x86_64-w64-mingw32-gcc (mingw-w64)	linking the EFI image (PE/COFF)	yes - the link gate skips
qemu-system-x86_64, OVMF (OVMF_CODE*.fd beside its OVMF_VARS*.fd), mtools, dosfstools	booting the image; the gates that measure a boot path	yes - boot gates skip
clang + wasm-ld	rebuilding the committed compiled-guest fixture	yes - the fixture gate skips
gnatprove	the SPARK proof	yes - reported as a skip
cargo-kani	the bounded-model-checking harness of the capability ledger	yes
A JRE	the TLA⁺ (TLC) and Alloy runners	yes
plantuml	rendering design/*.puml into the .svg files	yes

Two properties of the build host are load-bearing rather than incidental. The interpreter must not depend on a host math library - it does not: rounding, the square root and NaN normalisation are integer work over the bits, so two hosts compute the same bits. And the toolchain versions are what a stored run names: a result is comparable to another result from the same kind of host, and a run under software emulation is never compared with a run under hardware virtualisation.

6.2 Vendored dependencies, and why

The Rust workspace does not resolve crates from a registry at build time: src/rust/vendor/ carries 59 crates and src/rust/.cargo/config.toml replaces crates-io with that directory, with the lock file committed. cargo build and cargo test therefore work offline and produce the same bytes for the same lock file. Refreshing a dependency is an explicit act (cargo update -p <crate>, then cargo vendor src/rust/vendor), committed together with the tree that uses it.

The runtime-relevant third-party code is small and named: the ML-DSA-65 signature implementation (FIPS 204) that mesh and the wasi:crypto arm use, the ML-KEM and X25519 exchange behind the hybrid handshake, the hash and MAC primitives (blake3, keccak, hkdf, hmac), and heapless, which is what makes the forwarder's tables bounded. Everything else in the kernel - the interpreter, the MMU, the storage layer, the capability broker, the arbiter - is written in this tree.

6.3 References

• WebAssembly Core Specification (W3C) - the instruction set and validation rules the profile is a subset of: https://www.w3.org/TR/wasm-core-2/
• WASI - the system interface the host surface is written against, including the 0.3 async and stream shapes: https://wasi.dev/
• FIPS 204, Module-Lattice-Based Digital Signature Standard - the ML-DSA-65 scheme behind content signatures: https://csrc.nist.gov/pubs/fips/204/final
• UEFI Specification - boot services, the memory map, ExitBootServices and the calling convention the image is built for: https://uefi.org/specifications
• Dhrystone 2.1 (R. P. Weicker, 1988) - the integer workload the kernel's retired benchmark stages ran, ported to Ada/SPARK without changing its algorithms (TODOS.md item 28 moved the measurement off target; the unit left with it)
• TLA⁺ / TLC (L. Lamport) - the temporal models for epochs, fuel and the park lifecycle: https://lamport.azurewebsites.net/tla/tla.html
• Alloy 6 - the relational models for page tables and capability lifecycles: https://alloytools.org/
• Kani - bounded model checking for Rust, used for the capability-handle ledger: https://model-checking.github.io/kani/
• QEMU and OVMF (Open Virtual Machine Firmware) - the test machine and its firmware: https://www.qemu.org/, https://github.com/tianocore/edk2
• PlantUML - the diagram sources under design/ are PlantUML: https://plantuml.com/

---

7. Security, tests and enforcement

7.1 What the machine enforces

Security in Wolkie is not a mode a program can be put into; it is the set of things the hardware is configured to refuse, plus the set of things the kernel refuses by policy. Both are stated where they live, and the security-critical ones are contracts.

Boundary	Mechanism	Consequence of a violation
Address space	separate page-table roots per space (KPTI); a user root carries the user program plus a named, short list of supervisor pages the CPU needs for entry, exit, interrupt delivery and the TSS	the access faults; the fault class decides between contained, kill-the-run and kill-the-machine
Kernel code and data	never mapped into a user root as user-accessible; a user-accessible page is refused in a kernel space by policy	the manager refuses the mapping instead of trusting the caller
Writable and executable at once	no page is writable and executable at the same time (W^X)	a mapping that would need it is refused
Entry and exit	SYSCALL/SYSRET through a read-only trampoline page present in every root; a return to user mode via IRETQ is not used, because it would read the descriptor tables a user root must not expose	a malformed frame is a trap, not a privilege change
Authority	rights mask per run; object tokens minted by the broker and checked before the object is used; one live handle per space with monotonically rising ids (proved)	the call traps and the run rolls back
Work	fuel per instruction; a Tier-1 exhaustion traps; a Tier-2 park holds no budget and gets a fixed quota per event	a runaway module cannot outspend its grant
Memory edges	the seed stack and the interpreter's guest pages sit next to deliberately unmapped guard pages	an overflow faults at the boundary instead of landing in adjacent state
Provenance	content signatures (ML-DSA-65) verified against the signer's key; seeds derived from the build identity and salted with the space index, held in a sealed table with no read-back path	a block without an authenticating signature is not content this system serves
Shared mutable state	one writer per structure, locks defined at the HAL boundary in a documented order; the arch_smp_* gateways are serialised, because the state they touch is single-writer	a deadlock is a design error a reader can find, not a race to debug

7.2 What is not enforced

This is the part a security review should read first. The IOMMU, cache-way locking, the mesh replication model and the NVMe model are software models held against formal models and tests, not silicon enforcement. QEMU is launched with an emulated IOMMU device and an NVMe controller, but what the kernel does with them is a model of what a real IOMMU would do. The documentation states this wherever the claim appears, and this file claims no hardware guarantee it cannot demonstrate.

The interpreter is not proved either. It is a memory-safe Rust implementation held against bytecode the repository wrote and bytecode a real compiler emitted, and it refuses what it does not implement rather than approximating it. Where a claim rests on the interpreter, it is marked measured.

7.3 The gates

Every claim of the form "this works" is carried by a script that can fail. A gate has three outcomes - pass, fail, skip - and a skip (a missing tool, no writable accelerator) is never reported as a pass. What each verdict means, and the rule that a gate's stored verdict must agree with its exit status, is in docs/DEVELOPMENT.md.

Gate	What it establishes
scripts/test_all.sh	the aggregate: Ada harness, HASF ABI layer, GNATprove, every crate's tests, the C-ABI tests, the document gates, and the optional formal runners
scripts/prove/prove_spark.sh	GNATprove over the arbiter and the HAL protocols, with the flow and proof summary as the artefact
scripts/checks/check_abi.sh	no direct import crosses a language boundary; every crossing is an arch_*/vki_* gateway
scripts/checks/check_capability_bits.sh	the right bits the guest face uses agree with the ones the arbiter defines
scripts/checks/check_wit_bindings.sh	the committed WIT binding and the interpreter's canonical arms agree, number for number
scripts/checks/check_doc_counts.sh	the lists the architecture documents present as complete still match the code (host calls, commands, modules, and the stated bounds)
scripts/checks/check_console_help.sh	the console's help text names exactly the commands the dispatch has - the one surface an operator reads, read against the code; and the product profile and the text agree on which seven commands are mechanism proofs (--self-test plants that defect in a copy)
scripts/checks/check_apps_manifest.sh	apps/apps.manifest and the module trees agree: every source exists, every .wat has a row, no duplicate name, id or define - a module the build would silently skip, or two that answer one console number
scripts/checks/check_trace_paths.sh	every implementation path, and every relative link or image, in the model-to-code matrices and the architecture documents resolves
scripts/checks/check_code_citations.sh	a code citation in the developer documents lands on the symbol it names
scripts/checks/check_doc_headings.sh	a section pointer in a navigation document names a heading or a bold lead that document still has
scripts/checks/check_citations.sh	every cited stored run exists, and every stored run is cited by something
scripts/checks/check_comments.sh	no stale marker in a comment, no comment pointing at a path that no longer exists
scripts/checks/check_line_endings.sh	every source file is LF and UTF-8, so a byte-exact tool reads what the compiler read
scripts/tools/render_diagrams.sh --check	every design/*.puml parses; without --check it also writes the .svg
scripts/gates/run_boot_root.sh and its siblings	one boot path each: default root, MMU self-test, MMU switch, MMU fault, ring 3, CPL3 process, WASI 0.3 async wait, NDN, CMR, network ladder
scripts/prove/prove_kani.sh	bounded model checking of the capability-handle ledger
formal_verification/tla/verify_all.sh, formal_verification/alloy/verify_all.sh	the temporal and relational models, checked

A gate is never weakened to silence a false alarm: when a gate and the code disagree, one of them is wrong, and the documentation changes - not the threshold. The same rule applies to the failure direction of the kernel itself: an unhandled condition halts with a documented code instead of continuing in an unknown state.

7.4 Running it

Command	What it does
./scripts/build_all.sh	builds the crates, the kernel, the userspace modules the image embeds and the generated target configuration, then re-renders the diagrams; the EFI image itself is linked by the arch build (build_no_qemu.sh, or build_local.sh when it should also boot - both in src/ada_spark/core/boot/arch/x86_64/)
./scripts/test_all.sh	the full suite: language harnesses, proof, crate tests, C-ABI tests and the document gates
./scripts/prove/prove_spark.sh	GNATprove over the Ada/SPARK units
./scripts/tools/verify_touched.sh --list	prints the localized checks the current change owes, instead of guessing
./scripts/gates/run_qemu.sh	builds and boots the kernel interactively
./scripts/gates/run_boot_root.sh	the headless default-root boot gate (and the template for the path-specific ones)
./scripts/tools/clean_env.sh --dry-run	reports what a run left behind, without deleting anything

Two operational rules belong with them, because both were learned from a broken run. A boot always has a wall-clock timeout - an unattended guest that reaches its prompt and idles would otherwise hold the machine - and a run killed by that cap is a timeout, not a pass. One launcher at a time: a second build or QEMU next to a running one makes every artefact of the run indeterminate, so the scripts refuse to start instead of racing.

---

8. License

Wolkie Atto-Kernel is released under the GNU Affero General Public License, version 3 or later (AGPL-3.0-or-later). The full text is in LICENSE.

The license is a strong copyleft, and the "Affero" part is the reason it was chosen for a system of this shape: section 13 extends the source-code obligation to network use. If a modified version is run as a service that other users interact with over a network, those users are entitled to the corresponding source. For a kernel whose stated goal is verifiable behaviour, that matches the technical claim - a proof nobody can inspect because the source is closed would be a claim without evidence.

In practice:

• Using it - running, studying and modifying the kernel privately - is permitted without conditions.
• Distributing it, or a work based on it requires the same license and the source, including modifications.
• Offering it as a network service triggers the additional obligation to make the source of the version actually running available to the users of that service.
• No warranty. The program is provided as is; as a research prototype it must not be relied on for safety-critical use.

Third-party components keep their own licenses: the vendored crates under src/rust/vendor/ carry their upstream license files, and those terms apply to those files.

---

9. Repository layout

Path	Contents
src/ada_spark/core/main/	the arbiter: policy, per-core arbitration, console shell, process lifecycle, capability ledger, HAL protocols
src/ada_spark/core/boot/	the boot generator, the UEFI entry path, and arch/x86_64/: the HAL's C and assembly stubs, the interrupt path, the AP trampoline
src/rust/	the subsystem workspace: mmu, storage, arbiter_shim, drivers, mesh, ndn, ndn_guest, plus vendor/ and the committed lock file
src/wasm/	the interpreter and its host surface; wit/ holds the WASI 0.3 contract and its generated bindings, tests/fixtures/ the compiled guests it is held against
src/uefi_bundle/	the no_std Rust bundle linked into the EFI image
apps/wasm/	the user-space modules, one source per command or payload
tools/	host tools: wasm-runner (runs the profile off-target), kernel-bench (the memory measurement the kernel's retired benchmark reported), pqc-verify (re-derives a seed and verifies a printed signature), net-echo and ndn-responder (the peers the network gates talk to)
tests/rust-abi/	black-box C-ABI checks across the crate boundaries
formal_verification/	the TLA⁺ and Alloy models with their runners
design/	the PlantUML sources and their renders - the architecture, the boot sequence and the per-subsystem comparisons
scripts/	the automation, grouped by the question it answers: gates/ (one boot boundary each), checks/ (the host-side gates), build/, prove/, tests/, tools/, with test_all.sh, build_all.sh and common.sh at the root - the index is scripts/README.md
docs/	the measured developer detail, the round record, the verification mappings, and the stored runs

10. Terms used in this document

The complete list, with every abbreviation this tree uses, is docs/DEVELOPMENT.md -> "Abbreviations and names". These are the ones this document introduces.

Term	Meaning here
ABI	Application Binary Interface: the calling convention and data layout two compiled units agree on. Wolkie's only crossing is the C ABI, in the Windows x64 convention (arguments in RCX/RDX/R8/R9 plus 32 bytes of shadow space)
CMR	Causal Mesh Router: the layer that advertises and reconciles a node's epoch root hash over the NDN surface
CPL3	privilege level 3, i.e. user mode. The kernel runs at privilege level 0
CR3	the control register holding the physical address of the active page-table root
GDT / IDT / TSS	global descriptor table, interrupt descriptor table, task-state segment. The TSS supplies the stack a privilege transition lands on
HAL	Hardware Abstraction Layer: the only privileged layer. Instruction stubs are C or assembly; the protocols and every decision are Ada/SPARK
KPTI	Kernel Page-Table Isolation: separate kernel and user roots, with only the pages the CPU needs shared
ML-DSA-65	the module-lattice signature scheme of FIPS 204, used for content and space signatures
MMU	memory management unit: here, the paging structures and the Rust manager that owns them (src/rust/mmu)
NDN	Named Data Networking: content-named Interest and Data packets, with in-network reuse
SUH	State Update Hub: the immutable document a run publishes and a module can read
T-CAS	Tesseract Content-Addressed Storage: content addressed by hash, with time as a coordinate
Tier 1 / Tier 2	the two fuel tiers: one-shot and stateless, or parked with a fixed quota per event
UEFI	Unified Extensible Firmware Interface, the firmware that starts the kernel
VFS	virtual file system: the mapping from a path to an object and its content hash
WASI	WebAssembly System Interface, the standard the host surface is written against
WASM	WebAssembly, the instruction set user space is compiled to
WIT	WebAssembly Interface Types, the contract language src/wasm/wit/wolkie.wit is written in
W^X	the rule that no page is writable and executable at the same time

---

11. Hardware requirements

What a machine needs to run this kernel, and what the kernel costs on it, are the same question asked twice. The table below is measured from the tree on disk, not written by hand: scripts/tools/hw_requirements.sh reads the object sections, the embedded module payload and the interpreter's declared bounds, and writes the block between the two markers. ./scripts/tools/hw_requirements.sh --check re-derives it and fails when the table and the tree disagree, so a footprint cannot drift away from the build it describes.

Generated by ./scripts/tools/hw_requirements.sh from the tree on disk - do not edit by hand. Do not edit by hand: run the script, or --check to see whether the table still matches. A row whose artefact is absent here (a clean clone, or after a gate's cleanup) is skipped by --check, not failed - a measurement must not fail because the tree is in its initial state.

Requirement	Measured value	Source
EFI image on disk	2622 KiB	src/ada_spark/core/boot/arch/x86_64/boot.efi
Kernel code+data, loaded	1680 KiB	size over the Rust archives, the Ada objects and the C objects
Kernel .bss, zero-filled on the way up	4172 KiB	same
Kernel footprint, all sections	5 MiB	the two rows above
Guest modules embedded	23 module(s), 348 KiB	apps/wasm/build/*.wasm
Linear memory per run	2 MiB (256 pages x 2 halves)	MAX_MEMORY_PAGES
Engine region per instance	64 KiB (8 pages per half)	ENGINE_REGION_PAGES
Guest functions per module	at most 256	MAX_GUEST_FUNCTIONS
Host bindings per module	at most 30	MAX_HOST_BINDINGS
Operand stack	128 values	MAX_STACK_SIZE

Firmware and CPU, from the boot path itself: x86-64 with UEFI (the image is a PE32+ application started by boot_wrapper.S), SSE (the AP trampoline sets CR4.OSFXSR and OSXMMEXCPT; a core without them resets at bring-up), a local APIC (xAPIC or x2APIC), ACPI (the MADT walk that finds the cores) and a TSC. No GPU, no disk controller and no network card is required: storage and the mesh are modelled, and the console needs only a serial port (COM1) or the firmware's own console.

The derivation behind each row - which constant, which object file, which run - is in docs/DEVELOPMENT.md (docs/DEVELOPMENT.md -> "Where the system can get smaller, more portable or more frugal (the W-PROD-10 report)" for the measured levers, and its WASI inventory for the bounds). Nothing here is a hardware claim: the kernel enforces what the rows state, and the limits that are modelled rather than enforced are listed under Hard limits.

---

Where the detail lives

This file is the architecture: what the system is, which layers exist, how it boots, and what a module may do. The rest is carried by a small set of documents, each with exactly one job:

• docs/DEVELOPMENT.md - the measured developer detail: ABI signatures and return codes, every bound with its constant, proof figures, gate semantics, the lock discipline, and the run behind each number.
• docs/ROUNDS.md - the record: each round, the items it closed, and the artefact that proves each step.
• TODOS.md - the open work: the queue with the next step of each item, and the decisions that keep a closed item closed.
• AGENTS.md - the working agreement: where a change belongs, how it is built and tested, and the rules it has to satisfy.
• docs/VERIFICATION_MAPPING.md and docs/TRACEABILITY.md - the model-to-code traces.

A claim in this repository is worth exactly the evidence behind it: a proof, a model, or a stored run. Anything else is a hypothesis, and is labelled as one.