Comment Comment by robert_g Earlier post about SeL4 verification:https://news.ycombinator.com/item?id=23464187Also, 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-.... parent robert_g 6 years ago
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-....