Firstly, the entire classes of bugs that Haskell eliminates are not classes that are especially relevant to cryptography.
Secondly, if you know where someone has claimed that Haskell lets you "formally prove the code implements the spec" then please point it out to me so I can challenge them for being misleading at best.
Surprising that heartbleed got past you? Or does haskell not eliminate buffer overflows. I've heard many clam it does.
SeL4. It comes up regularly that C, or java or python or some other well used language doesn't work well with isabelle, coq because of pointers, destructive assignment or whatever but haskell is pure and this is one of the many advantage of pure. I don't have this opinion myself nor have I formed the opinion that it's false.
Secondly, if you know where someone has claimed that Haskell lets you "formally prove the code implements the spec" then please point it out to me so I can challenge them for being misleading at best.