Extending concurrent separation logic to the hardware level to verify the xv6 OS

A paper submitted to arXiv on 3 September 2026 by Nickolai Zeldovich and co-authors presents MachCSL, a framework that adapts Iris-based concurrent separation logic to reason about RISC-V hardware execution at the sub-instruction level, and uses LLM-based agents to verify the xv6 OS kernel (6,657 lines of C and assembly code). The verification uncovered 11 bugs in the xv6 implementation, one bug in the Sail RISC-V semantics, and one bug in Sail's Lean extraction, and took 102 days including framework development. The authors also prove a console-level theorem covering the kernel and the init, sh, echo, cat, grep, sync, and seccomp binaries in the initial file system image.

Computer Science Logic in Computer Science Submitted on 3 Sep 2026 v1 https://arxiv.org/abs/2609.04043v1 , last revised 12 Oct 2026 this version, v3 Title:Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents View PDF https://arxiv.org/pdf/2609.04043 HTML experimental https://arxiv.org/html/2609.04043v3 Abstract:MachCSL is a framework for verifying system software, such as an OS kernel, on top of low-level semantics of a RISC-V computer, based on the Sail RISC-V semantics. The key idea behind MachCSL is to adapt concurrent separation logic, based on Iris, to reasoning about low-level hardware execution at the sub-instruction level: page-table translation, TLB, privilege levels, configuration registers, instruction fetch/decode/execute, traps and interrupts, DMA, shared memory, power failures, etc. Reasoning at this level of detail ensures that the system software correctly manages all of the hardware details. Verifying software at this low level of abstraction is tedious, but LLM-based agents are capable of reasoning about such low-level details. As a case study, we verify the xv6 OS kernel 6,657 lines of C and assembly code , which provides a traditional Unix system call interface processes, file system, file descriptors, and preemptive scheduling and has substantial internal concurrency multi-core support with fine-grained locking, shared memory, interrupts, DMA, etc. . In the verification process, we uncovered 11 bugs in the xv6 implementation, as well as one bug in the Sail RISC-V semantics, and one bug in Sail's Lean extraction. The verification effort took us 102 days, including the time to develop the MachCSL framework. On top of the verified xv6 kernel, we prove a theorem about console-level behavior: e.g., if the user types echo hello world as input on the UART console, the only output the system can produce is hello world if there are no crashes or other errors . This theorem covers both the kernel and the init, sh, echo, cat, grep, sync, and seccomp binaries in the initial file system image. Submission history From: Nickolai Zeldovich view email https://arxiv.org/show-email/a54cf0b4/2609.04043 Thu, 3 Sep 2026 16:17:47 UTC 100 KB \ v1\ https://arxiv.org/abs/2609.04043v1 Sun, 20 Sep 2026 18:40:24 UTC 133 KB \ v2\ https://arxiv.org/abs/2609.04043v2 v3 Mon, 12 Oct 2026 01:10:25 UTC 138 KB Additional Features References & Citations Loading... Bibliographic and Citation Tools Bibliographic Explorer What is the Explorer? https://info.arxiv.org/labs/showcase.html arxiv-bibliographic-explorer Connected Papers What is Connected Papers? https://www.connectedpapers.com/about Litmaps What is Litmaps? https://www.litmaps.co/ scite Smart Citations What are Smart Citations? https://www.scite.ai/ Code, Data and Media Associated with this Article alphaXiv What is alphaXiv? https://alphaxiv.org/ CatalyzeX Code Finder for Papers What is CatalyzeX? https://www.catalyzex.com DagsHub What is DagsHub? https://dagshub.com/ Gotit.pub What is GotitPub? http://gotit.pub/faq Hugging Face What is Huggingface? https://huggingface.co/huggingface ScienceCast What is ScienceCast? https://sciencecast.org/welcome Demos Recommenders and Search Tools Influence Flower What are Influence Flowers? https://influencemap.cmlab.dev/ CORE Recommender What is CORE? https://core.ac.uk/services/recommender arXivLabs: experimental projects with community collaborators arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs https://info.arxiv.org/labs/index.html .