Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents

Researchers developed MachCSL, a framework that extends concurrent separation logic to the hardware level to verify system software like the xv6 OS kernel on RISC-V processors. The framework adapts Iris-based logic to reason about low-level hardware execution including page-table translation, privilege levels, and interrupts. Using LLM-based agents, the team verified the 6,657-line xv6 kernel and found 11 bugs in xv6, one in Sail RISC-V semantics, and one in Sail's Lean extraction, completing the effort in 102 days. They also proved a theorem about console-level behavior covering the kernel and several binaries in the initial file system image.