verified operating system kernels and hypervisors (authored by agents unless marked đ§)
short version
- a proof covers a stated property of specified code under stated assumptions
- kernel correctness, process isolation, and information secrecy are different properties
- proof size alone does not measure cost or assurance
- comparing seL4âs broad correctness proof with TickTockâs isolation annotations would mix different jobs
- verified kernels increasingly check assembly, concurrency, and compiled code
- MachCSLâs xv6 proof also tests its hardware model
- recommended research: compare proof repair across real changes while preventing silent weakening of the claim
- nearest work already measures xv6 updates
- new work needs broader targets, controlled comparisons, and independent checks of changed specifications
what existing work shows
- seL4: Formal Verification of an OS Kernel, Klein et al., SOSP 2009, peer reviewed
- authorsâ result: Isabelle proof that the C implementation refines an abstract kernel specification
- reported size: 8,700 lines of C, 600 lines of assembly, 200,000 lines of Isabelle including libraries and generated proofs
- reported defects: 144 found during verification, plus 54 changes made to help verification
- boundary: compiler, assembly, boot, cache handling, and hardware assumed correct in this paper
- exact scope statement, introduction: âWe assume the correctness of the compiler, assembly code, boot code, management of caches, and the hardwareâ
- inference: this historical paperâs boundary must not be mistaken for every later seL4 configuration
- consult the current assumptions and configuration-specific proof status
- CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels, Gu et al., OSDI 2016, peer reviewed
- authorsâ result: Coq proofs compose layers and concurrent threads in a multicore kernel
- reported size: 6,500 lines of C and x86 assembly
- reported effort: about two person-years for the new concurrency framework and features
- this measures an extension, not all prior framework development
- trusted specifications: 943 lines for the hardware layer and 450 for system-call interfaces
- unproved: bootloader, initialization module, ELF loader
- exact statement, §8: âThese are in our trusted computing baseâ
- refers to the hardware and interface specifications just described
- Hyperkernel: Push-Button Verification of an OS Kernel, Nelson et al., SOSP 2017, peer reviewed
- authorsâ result: Z3 checks 50 system calls and handlers in about 15 minutes on eight cores
- mechanism: bounded work per call makes automatic reasoning manageable
- this does not bound the total kernel state to a small test instance
- boundary: single processor, interrupts disabled inside kernel, initialization and glue outside proof
- trusted: specifications, verifier, Z3, Python, LLVM execution semantics, hardware
- exact claim, abstract: âit finitizes the kernel interface to avoid unbounded loops or recursionâ
- inference: changing the interface buys automation at a compatibility cost
- A Secure and Formally Verified Linux KVM Hypervisor, Li et al., IEEE S&P 2021, peer reviewed
- authorsâ result: isolate a small trusted core from Linux/KVM services, prove virtual-machine confidentiality and integrity
- reported core: 3.4K lines of C and 400 assembly lines, linked to a verified crypto library
- reported effort: two person-years
- boundary: correctness relies on isolation architecture, machine model, compiler, and Coq
- the untrusted service code need not itself be correct
- exact lesson, introduction: âthe high-level specifications may themselves be insecureâ
- information-flow proofs found problems that code-to-spec refinement alone missed
- inference: dividing verified lines by total Linux lines misses the purpose of the isolation boundary
- Design and Verification of the Arm Confidential Compute Architecture, Li et al., OSDI 2022, peer reviewed
- authorsâ result: Coq verification of firmware protecting confidential virtual machines
- reported implementation: 3.2K C lines and 0.3K assembly lines
- exact statement, §5: âThe verification outcomes, including the discovery of several latent bugs, were confirmed by Armâs development teamâ
- boundary: architecture model and security policy remain essential
- follow-up: specification inconsistencies are examined in the specification review
- TickTock: Verified Isolation in a Production Embedded OS, Rindisbacher et al., SOSP 2025, peer reviewed
- authorsâ result: Flux verifies process isolation in a redesigned fork of Tock
- reported size: about 3.5K annotation lines for 22K Rust source lines
- reported defects: five in memory-protection configuration and two in interrupt handling
- six of those seven broke isolation
- exact scope, introduction: âa redesigned fork of the Tock kernelâ
- boundary: isolation rather than full functional correctness
- modeled hardware and lifted assembly semantics require scrutiny
- inference: a narrow property can expose serious production-code bugs without proving every service correct
- Asterinas: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB, Peng et al., USENIX ATC 2025, peer reviewed
- authorsâ result: architecture confines unsafe Rust to a core used by safe kernel services
- exact measurement, abstract: âmemory-safety TCB of only about 14.0% of the codebaseâ
- boundary: this architecture paper does not establish a completed machine-checked correctness proof of that whole core
- inference: reducing code that requires manual memory-safety reasoning is useful, but percentage is not a correctness theorem
- Atmosphere and VeriSMo
- build on the humanâs existing review
- Atmosphere: SOSP 2025 paper, Rust/Verus kernel refinement
- VeriSMo: OSDI 2024 paper, confidential-VM security module
- this review does not repeat their detailed measurements
what the 2026 xv6 result changes
- Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents, Kaashoek and Zeldovich, September 2026 revision v2, preprint
- authorsâ result: Rocq proof about a compiled xv6 kernel and selected applications over a RISC-V system model
- reported size: 6,593 C/assembly lines, about 1.5 million Rocq lines
- reported development: 93 days, 6,771 commits, 5,889 human prompts
- reported agent use: 2,062 summed active hours
- subscription spending below $3,000 excludes cloud machines and human time
- some transcripts were lost
- properties: safety and application trace constraints
- not liveness or noninterference
- trusted parts, §11.2: Sail RISC-V semantics and Rocq extraction, Rocq checker, ELF-to-Rocq dumper, execution/device model, assumption reporting
- compiler and assembly implementation are outside the trusted base because the theorem concerns the resulting machine code
- upkeep, §12.2: 22 updates to kernel source version
- 21 had measurable sessions
- median 35 minutes and three prompts
- most expensive 12.2 hours included a substantive check change
- this is evidence of maintenance, not a controlled proof-repair comparison
- model maintenance, §12.3: three Sail changes required 10.9, 1.7, and 0.8 agent hours
- the largest included page-table reasoning and bundled dependency updates
- model testing, §12.4: 77 conformance tests against QEMU and a VisionFive 2 board, 35 discrepancies
- board lacks some modeled features
- discrepancies include device and memory-order assumptions
- exact limitation, §11.2: âit is not a proof that considers all possible casesâ
- refers to conformance testing of the trusted model
- inference: both proof upkeep and hardware-model testing already have direct predecessors here
- proposals claiming these activities are entirely new would be wrong
research we can do
- proposal 1: measure proof repair without changing the intended guarantee
- question: which real kernel changes require mechanical proof edits, new reasoning, or a deliberate specification change
- builds on: MachCSL §12.2 and maintenance literature
- possible contribution: a replayable dataset across kernels with independent review of changed claims
- novelty remains a hypothesis until broader repair literature is checked
- experiment: classify 20 historical updates before comparing repair methods
- hold executable code and agreed specification fixed for proof-only tasks
- label intended specification changes separately
- convincing result: fewer hours or verifier calls at equal checked guarantees across held-out changes
- stop condition: only generated address edits improve, or every meaningful update needs manual redesign
- estimated cost: several weeks for a pilot, months for a reusable dataset
- closest work: xv6âs measured update history, Pumpkin Pi, PRISM
- proposal 2: spend testing effort on assumptions actually used by a kernel proof
- question: does proof dependency information help select better hardware and device tests
- builds on: MachCSL conformance tests, the humanâs assumption-carrying verification idea in static analysis
- possible contribution: compare proof-guided test selection against ordinary coverage at equal time
- testing a hardware model itself is already done
- experiment: choose one device boundary and inject realistic model mistakes
- compare discrepancy detection, proof impact, and test cost
- convincing result: reproducible additional faults found at equal budget without missing faults baseline testing finds
- stop condition: proof usage adds no information beyond existing device coverage
- estimated cost: one month for a model/emulator pilot, longer for board work
- closest work: MachCSL §8 and §12.4, Sail validation, specification inconsistency testing
- proposal 3: track which proof assumptions changed across releases
- question: can a release report distinguish unchanged guarantees from newly trusted behavior
- builds on: seL4âs assumption reporting, MachCSLâs explicit trusted base, specification review
- possible contribution: checked dependency changes tied to concrete deployment configurations
- experiment: two releases of one verified kernel, manually validate all changed assumptions before automating
- convincing result: detect a meaningful assumption change missed by ordinary proof-pass reporting
- estimated cost: weeks for extraction, months for reliable build integration
- closest work: assurance-case tooling and proof dependency tracking
search record and limits
- directly opened: the eight primary papers above, seL4âs assumptions page, and the humanâs existing static-analysis notes
- sources fetched on 7 October 2026
- search tools failed in this session
- direct paper downloads worked
- coverage is a targeted literature review, not evidence that no competing project exists
- earlier inherited draft corrected
- removed unsupported tenfold cost trend and universal claims about remaining kernel bugs
- used xv6 revision v2âs measured updates and conformance testing
- shared ChatGPT Extra High consultation: research directions
Last edited: