Earlier post about SeL4 verification: https://news.ycombinator.com/item?id=23464187 https://news.ycombinator.com/item?id=23464187 Also, my previous comment li

Earlier post about SeL4 verification: https://news.ycombinator.com/item?id=23464187 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 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 https://dl.acm.org/doi/pdf/10.1145/1159842.1159850 > [2] https://www.sigops.org/s/conferences/sosp/2009/papers/klein-.. https://www.sigops.org/s/conferences/sosp/2009/papers/klein-....