World’s first formal machine-checked proof of a general-purpose operating system kernel.
Haskell played a pivotal role in achieving this results. The Haskell kernel model described in our 2006 Haskell Workshop paper formed the basis for the verified high-performance C implementation and the kernel model used for verification — for details, see Klein et al.’s forthcoming SOSP paper.
