Hacker News Reader

There is already a formally verified kernel - https://sel4.systems/home.pml

That's very important work, but I don't think it includes many of the features we would associate with an operating system.

It's hard to overstate how (intentionally) tiny it is compared to something like Linux or a BSD kernel.

I didn't know that existed. What a fantastic project. Thanks for the link.