Definition
Plain language
An operating-system core with a mathematical proof that it has no bugs of a certain kind.
As stated in the literature
A formally verified microkernel with a machine-checked proof of functional correctness against its specification; a landmark example of verified systems requiring years of expert effort.
Why it matters: It demonstrates that critical software can be proven correct, but the years of expert effort it took show how costly such guarantees still are.
For example, it comes with a machine-checked proof that the core of the operating system behaves exactly as specified, with no functional bugs.
Heard on the show
“The seL4 microkernel, CompCert — a verified C compiler — IronFleet for distributed consensus, Chapar for causally-consistent storage.”Episode 075 — Growing Code and Proof Together: Verified Systems in Ten Hours Instead of a Year