World’s first formal machine-checked proof of a general-purpose operating system kernel

World’s first formal machine-checked proof of a general-purpose operating system kernel from Planet Haskell.

Some previous work has been mentioned here before, but I don't think there has been a story on any of the previous work.