Mechanically Assured Kernel Components: Safe and Correct by Construction, in the Age of Coding Agents

Abstract

A society that runs on software needs a reliable foundation, and the operating system kernel is one of its cornerstones. Yet the kernel is difficult to get right, owing to a fundamental gap between its inherent complexity and the assurance that the community can provide. Coding agents widen this gap: code production has become mechanical, whereas assurance still relies on a human process. Vulnerabilities and safety issues are consequently reported by the thousands every year, and their number is rising rapidly with the recent surge in code production.

In this talk, we show that machine-produced code can be machine-checked by rigorous, automated formal reasoning, making kernel components safe and correct by construction. Because such assurance is mechanical, it keeps pace with the kernel's growth while providing the formal guarantees that privileged code demands. We present a line of work on the verifier that runs inside the Linux kernel and gates every component loaded into it. We show how a decoupled design attains precision on demand, with proofs constructed in user space and checked in the kernel, and how the verifier itself can be made robust and trusted less. As AI progressively lifts the proof burden, more ambitious goals come within reach, from machine-derived, machine-proved algorithms now making their way into Linux to end-to-end verified kernel components. We conclude with the next steps toward a reliable and performant kernel, and beyond.