SlopOS

---

This Is Not QEMU

That is a real laptop. The desktop — compositor, terminal, text editor, file manager, system monitor, image viewer — is drawn by our own Intel Xe display driver. The keyboard and I²C-HID touchpad were discovered by walking the firmware's actual AML tables with our own ACPI interpreter, then driven over our own I²C and GPIO drivers. The slop has escaped the sandbox.

---

Get It Running

You need: QEMU, xorriso, e2fsprogs, just — plus Go ≥ 1.22 if you want just test, and openssl for just test-host's TLS interop tests

# macOS
brew install qemu xorriso e2fsprogs just go

# Debian/Ubuntu
sudo apt install qemu-system-x86 xorriso e2fsprogs golang
cargo install just  # or: https://github.com/casey/just#installation

# Arch (btw)
sudo pacman -S qemu-full xorriso e2fsprogs just go

# Then:
just setup          # installs the pinned rust nightly + the forked `slopos` sysroot
just boot-live      # spins the wheel, from RAM

Command	What it does
just boot	Boot the development machine, wheel first: a persistent / carrying the toolchain and a clone of this checkout. Also needs clang, lld, cmake, ninja, util-linux (sfdisk), dosfstools and mtools
just boot-fast	just boot without the Wheel of Fate (coward)
just boot-live	Boot the live ISO from RAM in a window, as bare metal runs it; nothing persists. ROULETTE=0 skips the wheel
just test	Run the test suite — thousands of tests — under QEMU
just --list	Everything else (there's a lot)

To build SlopOS inside SlopOS, cross-build the toolchain once (just toolchain, hours), just boot, and in the guest:

cd /src/slopos && scripts/selfhost.sh install   # the new base runs at once
scripts/selfhost.sh install-kernel              # only for a kernel change
bootctl reboot      # boots the new kernel once; `bootctl commit` keeps it

When it wedges, ask it why: press SysRq (Alt+PrintScreen) — or send a BREAK on the serial line — then a command key. h lists them; t dumps every task with a symbolized park site. Only the physical console can trigger it, and kconsole=off on the kernel cmdline turns it off entirely.

When an installed system will not come back, boot the live ISO and type shell --rescue: one consent at the machine gives a root shell there that can e2fsck and mount the installed disk and repair its boot partition with bootctl --boot /dev/<boot partition> base rollback.

QEMU_DISPLAY=cocoa just boot                       # force a display backend (macOS auto-detects Cocoa)
QEMU_FB_WIDTH=2560 QEMU_FB_HEIGHT=1440 just boot   # manual framebuffer override
VIDEO=0 just boot                                  # serial only, no window
ROULETTE=0 just boot-live                          # the live ISO without the Wheel of Fate
just ports=7777,8080 boot                          # expose guest ports on the host
just test 'mm::*'                                  # run a subset of the tests
just boot-debug                                    # QEMU GDB stub on :1234

---

What's In The Slop

Everything below is #![no_std] Rust written for this kernel — no smoltcp, no borrowed driver crates. When we say the wizards wrote a TCP stack, we mean the wizards wrote a TCP stack.

Kernel — SMP preemptive scheduler, buddy allocator with demand paging and copy-on-write fork, SYSCALL/SYSRET fast path, LAPIC/IOAPIC + MSI-X interrupts, futexes, signals, pipes, ppoll, PTYs, process groups, signalfd, pidfd. A panic gets caught, its backtrace symbolized, and the damage billed to the offending task's oops ledger — the machine keeps going.

Drivers — Intel Xe display (the one in the photo), virtio-gpu/blk/net, i8042 keyboard with live layout switching (the Swiss QWERTZ in the photo types its dead keys correctly), and an I²C-HID touchpad sitting on our own DesignWare I²C and Intel GPIO drivers, wired up by our own ACPI/AML interpreter.

Network — a from-scratch TCP/IP stack: ARP, IPv4, TCP, UDP, ICMP, DHCP, DNS, unix sockets, NAPI-style ingress. Userland ships curl, ping, nc, and — for auditing your own two sockets — nmap.

Desktop — a compositor with damage tracking and occlusion culling, clients passing buffers over memfd + SCM_RIGHTS (the Wayland trick), an appkit widget toolkit that draws proportional UI text beside a fixed-cell code surface, and apps: terminal (with scrollback reflow), a code editor with a file tree, syntax highlighting and a command palette, file manager, image viewer, system monitor.

Plumbing — our own libc (slibc) with an mmap-only malloc, an io_uring-style submission ring (SlopRing), a VFS with ext4, devfs, ramfs, and an initramfs RAM root that boots with no disk attached at all.

The economy — the Wheel of Fate gates every boot, and outcomes accrue to your W/L balance. The only operating system with a load-bearing gambling mechanic.

---

Actually, The Slop Is Proven

Under the goofy exterior, SlopOS is a framekernel: every line of unsafe in the entire kernel is authored in one trusted crate, slopos-ostd. Every other kernel crate is #![forbid(unsafe_code)], and because a macro from another crate can expand unsafe past that lint without a diagnostic, CI also expands every kernel crate and reads what the compiler actually saw — zero executable unsafe, and unsafe impl / link_section / no_mangle only from a named list with a reason attached to each. Alongside it, gates inspect the final ELF: no stack frame over 2 KiB, no SSE instruction anywhere in the kernel, every linker registry holding whole entries.

The number worth defending is not the keyword count — folding unsafe behind a safe wrapper is the design, not a cheat. It is how much of OSTD's API you have to trust by reading rather than by type-checking: 52 pub unsafe fn, 15 pub unsafe trait, and no safe function that carries a prose contract — a CI ratchet keeps that last number at zero. just tcb-ratio reports unsafe-line density (0.31 %, gated at 1 %) — useful as a trend, not comparable to other projects' TCB fractions, which are measured differently.

The load-bearing invariants of that core are machine-checked with Verus, an SMT-backed proof system for Rust. The proofs cover the spots where a bug would be genuine undefined behaviour rather than a typed error:

• Frame reference counts — no double-free, no use-after-free.
• Slab slot lifetimes — a slot can never outlive the slab it came from.
• Page-table mutation — every walk stays well-formed; user mappings can't reach into sensitive kernel memory.
• SlopRing cursors & buffer pool — a hostile userland can't overwrite or overflow the shared rings.
• TCP zero-copy pinning — a page stays pinned as long as the NIC might still read it.

The proofs run in CI on every change and reproduce locally with just verify. For everything they don't cover: thousands of tests boot under QEMU on every change (just test), the trusted core runs under Miri (just check-miri), and when a bug only reproduces on Tuesdays, there's deterministic time-travel debugging (just rr-record / just rr-replay).

---

The Wizards Invented None Of This

Nobody thinks up demand paging on a beach. Every genuinely hard problem in this repo — paging, preemption, wake races, TLB coherence, TCP over a network that hates you — was solved decades before we got here by people who wrote it down and gave it away. The wizards washed up on Sloptopia with no operating system and a spectacularly well-stocked library. We studied and reimplemented. We did not copy. The ideas are theirs; only the slop is ours.

Asterinas — the shape of this entire kernel. The framekernel thesis is theirs: one trusted crate owns every line of unsafe, everything else is #![forbid(unsafe_code)], and your TCB size is a number you are expected to defend in public. So is the name slopos-ostd, the vocabulary our memory manager speaks all day (MetaSlot, Frame<M>, VmSpace + cursors, derive(Pod)), and the 2 KiB stack ceiling CI fails builds over — Inv. 5′, out of §4.3 of their ATC '25 paper. Their KernMiri and vostd work is why we believed the proofs above were worth attempting rather than merely hoping at.

Linux — the largest debt by a distance. The errnos, signals, termios and io_uring ABI are the obvious part. The rest is everything we only got right because Linux got there first: try_to_wake_up's totality discipline, the 16-slot PCID scheme from arch/x86/mm/tlb.c, call_rcu, lockdep, the n_tty line discipline, the VFS shape, the CSPRNG from drivers/char/random.c, NAPI ingress, and a TCP stack that inherited its timers from thirty years of other people's outages. Our tests speak KTAP; our stack gate is CONFIG_FRAME_WARN with the warning promoted to a build failure.

Redox — how a Rust OS models an address space without unsafe: a BTreeMap of regions with enum backings, which is what our VMA layer still is. Also the per-CPU control region, the PS/2 init sequence, and the standing proof that a from-scratch Rust OS is a thing people actually finish — load-bearing knowledge when your kernel has failed to boot nine times in an evening.

Also read closely, each for something specific — CortenMM (SOSP '25 best paper) for the page-table cursor and the invariants our proof discharges; Fuchsia for SafeStack's pinned per-thread TLS offsets; FreeBSD for WITNESS lock-order checking and stop_cpus_hard; illumos for cv_wait_sig's return semantics; seL4 for the queued-bit discipline and the older idea that an invariant is a thing you prove; Rust for Linux for Opaque<T>, and for pin-init, read very closely before we wrote our own Init<T, E>; musl for the __init_tls auxv walk; and smoltcp — still not a dependency, as advertised above — which settled typestate vs. enum for our TCP sockets.

Standards and tools — Wayland (the memfd

• SCM_RIGHTS buffer handoff is libwayland's trick), POSIX, VirtIO, the ext4 on-disk format, a couple dozen IETF RFCs, VT100/xterm escapes, ACPI, UEFI and the Intel SDM; built and checked with Limine, QEMU, OVMF, Verus, Miri, rr, just and Go — and Rust, without which this project's entire security argument, the compiler won't let us, would just be a wish.

And the honest one, because leaving it out would be cowardly: SlopOS was built with an enormous amount of AI assistance, and the models doing that writing learned how kernels work by reading the projects credited above. When a model hands the wizards a wake path with the right totality argument, that is not magic — that is someone having gotten it right in public, years ago, at length. Same debt as always. It just arrives faster now.

---