Rust / x86_64 / framekernel
An operating system written by AI agents.
We named it slop, then made the build prove otherwise. Verus checks the invariants the kernel rests on.
A real laptop. Our own Intel Xe driver lights that panel, and our ACPI interpreter found the touchpad.
Do not take the machine's word for it.
An agent will tell you the code is correct. That is worth nothing, so we made the build prove it. slopos-ostd owns every unsafe block and the other crates carry #![forbid(unsafe_code)]. A macro can smuggle unsafe past that lint without warning, so CI expands each crate and reads what the compiler saw.
pub unsafe fn
pub unsafe trait
That is the whole trusted surface. No safe function leans on a # Safety note to stay sound, and the build fails if one appears.
Verus, an SMT-backed proof system for Rust, checks the invariants underneath that crate. The proofs cover the spots where a bug corrupts memory instead of raising a type error.
- Frame reference counts. No double-free, no use-after-free.
- Slab slot lifetimes. A slot cannot outlive the slab it came from.
- Page-table walks. User mappings cannot reach kernel memory.
- SlopRing cursors. A hostile userland cannot overflow the shared rings.
- TCP zero-copy pinning. A page stays pinned while the NIC can still read it.
The agents wrote a TCP stack.
SlopOS pulls in no networking or driver crates, so the retransmit timers, the AML interpreter and the compositor are #![no_std] Rust written for this kernel. The models learned how kernels work by reading Linux, Asterinas and Redox. We credit that debt in the source.
# five commands to a booted OS git clone https://github.com/SlopLabs/slopos.git cd slopos just setup # pinned rust nightly just boot # spins the wheel just test # 3,000+ tests under QEMU root@sloptopia:/#
Kernel
An SMP preemptive scheduler, demand paging with copy-on-write fork, futexes, signals, PTYs and pidfd. When a task panics, the kernel symbolizes the backtrace, bills the damage to that task and keeps running.
Drivers
Our ACPI interpreter walks the firmware's AML tables to find the touchpad, then drives it over our own I²C and GPIO. The Intel Xe driver paints the panel in that photo.
Network
ARP, IPv4, TCP, UDP, ICMP, DHCP, DNS and unix sockets, with NAPI-style ingress. Userland ships curl, ping, nc, and nmap for auditing your own two sockets.
Desktop
Clients hand the compositor their buffers over memfd and SCM_RIGHTS, the way Wayland does it. It tracks damage, culls what you cannot see, and runs four applications.
The bootloader gambles with your session.
Before the desktop starts, SlopOS spins the Wheel of Fate and charges the result to your W/L balance. We shipped the joke and then had to live with it. Run just boot-fast to skip the spin.
Documentation
These pages say what works today, which parts we made strange on purpose, and where the source still disagrees with the prose.
The name is a warning.
POSIX coverage stops well short of complete, and the hardware list runs to one laptop and a QEMU target. The status pages name the edges you will hit before you hit them.