AI agents help formally verify the xv6 kernel down to the hardware level

Frans Kaashoek and Nickolai Zeldovich have presented MachCSL, a framework for formally verifying system software on top of the low-level semantics of a RISC-V computer. It builds on the official Sail RISC-V semantics.

Reasoning at the hardware level

The core idea of MachCSL is to adapt concurrent separation logic (based on Iris) to reasoning about hardware execution at the sub-instruction level. These are the details usually hidden behind abstractions: page-table translation, the TLB, privilege levels, configuration registers, the instruction fetch/decode/execute cycle, traps and interrupts, DMA, shared memory and even power failures. Reasoning at this level of detail guarantees that the system code correctly manages every hardware subtlety.

Verification at such a low level of abstraction is tedious for a human — but, the authors note, LLM-based agents turn out to be rather good at reasoning about exactly these minutiae. They shouldered much of the grind.

The xv6 case study

As a demonstration, the researchers verified the xv6 teaching kernel — 6,657 lines of C and assembly. The kernel offers a traditional Unix system-call interface (processes, a file system, file descriptors, preemptive scheduling) and carries substantial internal concurrency: multi-core support with fine-grained locking, shared memory, interrupts, DMA.

Along the way they uncovered 11 bugs in the xv6 implementation itself, plus one bug in the Sail RISC-V semantics and one in its Lean extraction. The whole effort took 102 days — including the time to build the MachCSL framework.

The echo theorem

On top of the verified kernel the authors proved a theorem about console-level behavior. If the user types echo hello world on the UART console, the only output the system can produce is hello world (absent crashes or other errors). The theorem covers not just the kernel but also the init, sh, echo, cat, grep, sync and seccomp binaries in the initial file-system image.

Source: Lobsters