Probably one of the coolest uses of Haskell in verification is as the high level model implementation of sel4, where a theorem prover embedding is used to prove

Probably one of the coolest uses of Haskell in verification is as the high level model implementation of sel4, where a theorem prover embedding is used to prove that the c impl of sel4 microkernel operating system is basically just a more detailed refinement of the Haskell description!