Comment by alokedesai

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.