This is cool because it's in Haskell, but there are a bunch of great formal theorem provers, coq (https://coq.inria.fr/) being one of the most famous ones.
I would like to emphasize that this gives you a theorem prover "inside" haskell, unlike coq/agda where you need to do program extraction. This means you can combine proofs and programs without a significant impact to the runtime performance.