Earlier post about SeL4 verification:

https://news.ycombinator.com/item?id=23464187

Also, my previous comment linking to how SeL4 performed the verification:

https://news.ycombinator.com/item?id=23475748

> seL4 hey used Haskell to create an model which was then their specification to help with the formal verification process [1][2].

> [1] https://dl.acm.org/doi/pdf/10.1145/1159842.1159850

> [2] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-....