---
format: "aidr-story-markdown/v1"
id: "23f55e8b53b2d0605bcd00b02f6c906505204628cda42c280b86bd4639b596a3"
canonical_url: "https://aidr.today/23f55e8b?lang=en"
title: "Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents"
lang: "en"
requested_lang: "en"
available_langs: ["en","vi"]
translation_fallback: null
fallback_fields: []
published_at: "2026-10-22T04:47:01.000Z"
category: "Research"
topics: ["agent"]
source_urls: ["https://arxiv.org/abs/2609.04043","https://lobste.rs/s/puijfw/extending_concurrent_separation_logic"]
summary: "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."
---

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

> [Open the canonical story](<https://aidr.today/23f55e8b?lang=en>)

**Published:** 2026-10-22T04:47:01.000Z
**Category:** Research
**Topics:** agent

## Summary

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\.

## Sources

- [Story source](<https://arxiv.org/abs/2609.04043>)
- [Discussion](<https://lobste.rs/s/puijfw/extending_concurrent_separation_logic>)