AI-assisted proofs reach down to computer hardware
- What it is
- The paper reports AI-agent-assisted formal verification of an xv6 operating-system kernel down to RISC-V hardware semantics.
- Who did it
- M. Frans Kaashoek and Nickolai Zeldovich
- What it could mean
- Could your next computer ship with fewer hidden bugs? This teaching-kernel project points toward AI-assisted proofs that, if the approach scales, could catch low-level mistakes before software reaches real devices.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents ↗See the proposed checks
Obtain a source-pinned MachCSL/Iris/Sail/xv6 artifact if released; identify the exact xv6 and Sail revisions; replay the stated verification with proof-assistant kernel checks; map the 6,593-line scope and each reported bug to the specification; and independently examination hardware-model, concurrency, DMA, and agent-generated-proof trust boundaries.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
Following the proof down to the machine
The layers connect kernel code, memory resources and processor behavior. MachCSL extends separation-logic reasoning to detailed RISC-V execution, including behavior below a single instruction. The illustration explains the levels involved; it is not an actual chip layout or a verification result.
Read the source · Abstract · MachCSL and low-level RISC-V semantics ↗- What it claims
- The authors introduce MachCSL, adapting Iris-style concurrent separation logic to Sail RISC-V sub-instruction semantics, and report an AI-agent-assisted verification of a 6,593-line xv6 kernel implementation that found nine xv6 bugs and one Sail-semantics bug. It squarely tests whether LLM agents can contribute to reviewable low-level formal verification while the source is current.
- Why this could matter
- AI-assisted proofs reach down to computer hardware Operating systems make devices usable, but their deepest rules must survive memory, interrupts, and hardware translation. This paper claims AI agents helped verify a real teaching kernel at that level, while uncovering implementation and specification bugs.
- If it holds up
- Methods: it would offer a concrete model for combining formal hardware semantics, human-designed invariants, and machine assistance in reviewable systems verification; reuse elsewhere still requires released artifacts and independent replay.
- If it does not
- The claimed verification scope or bug findings would narrow, showing which model, proof boundary, or AI-produced step needs stronger evidence before such workflows are trusted.
- Impact horizon
- Methods · Formal verification · Operating systems · AI-assisted proof
- Version
- submitted 2026-09-03 16:17:47 UTC
- Why we tracked it
- a fresh, unusually consequential AI-assisted formal-methods claim with specific reported scope and bug findings, but no source-linked repository, proof scripts, or independently replayable artifact on the primary record; no docket created.
- Highest-risk dependency
- The abstract does not identify the proof assistant, the released proof objects, the exact source revisions, the nine kernel bugs, or how agent output was checked. Without those artifacts, the claimed coverage, bug findings, and reliability of the AI-assisted proof workflow are not independently assessable.
- Available artifacts
- arXiv supplies PDF, experimental HTML, and TeX source. No public repository, proof-assistant project, version-pinned script, proof object, or bug-fix set is linked on the primary record at retrieval. No artifact was downloaded or executed.
- Current boundary
- Intake record only; examination not started.