Then we build the gates that check what comes back. So far that has produced an operating system that boots.
SlopOS on a real laptop, drawn by a display driver the agents wrote.
Letting a model write a kernel is the easy part. The work is deciding what to point it at, and proving afterwards that the result holds.
A person picks the problem, argues about the architecture, and rejects the approach when it is wrong. Nobody here hand-writes the implementation.
Confidence is free for a model to produce, so we do not take it as evidence. SlopOS answers to Verus proofs, Miri and a few thousand tests that boot under QEMU on every change.
Every repository is public from the first commit, including the parts that do not work yet. SlopOS keeps a written list of its own known limitations.
A framekernel in Rust with its own TCP stack, ACPI interpreter, display driver and compositor. One crate holds every line of unsafe, and Verus proves the invariants underneath it. The docs site explains how those gates work and what still breaks.
