Comment by robert_g

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-...