A bit late to the party here, but wanted to chime in since @ocramz mentioned SBV.
Formal verification of Haskell code remains elusive. Every system I know of have caveats, and SBV is no different: It needs you to “squint” in a particular way, and buy into certain assumptions. Also, you get a huge trusted code base. (Not just SBV itself, but also the underlying SMT solver which is not verified in any sense of the word. Though they are quite reliable!)
Up until recently SBV remained a push-button tool: You expressed your problem, and hoped that the solver gave you an answer in a reasonable amount of time. This mostly works if your problem is over bit-vectors or other basic types, you didn’t need any “interesting” use of quantifiers, and the proof did not need induction. Alas, most interesting Haskell functions are recursion, and any interesting property of a recursive definition will require induction.
A more recent development in SBV is support for more user-guidance in proofs, and support for induction. It still has all the SBV quirks, but the user now gets to tell the solver how to build the proof. This is similar to how theorem provers like Isabelle/ACL2/Lean etc., work, but of course in a sense more primitive. But it has the advantage of relying on all the decision procedures the underlying solver knows, and remains entirely within Haskell.
There are many examples that come with the latest release, to demonstrate:
- Merge sort: Documentation.SBV.Examples.TP.MergeSort
- Quick sort: Documentation.SBV.Examples.TP.QuickSort
- A plethora of list-processing function proofs: Data.SBV.TP.List
- Boyer-Moore majority algorithm correctness: Documentation.SBV.Examples.TP.Majority
Can this be used for proofs of “production-code” Haskell? No, not right now. It’s mostly an intellectual exercise, and I suppose it’s good for teaching and personal enjoyment. But the state of affairs improve with each day.
Happy hacking!