Liquid Haskell

Liquid Haskell allows to annotate code with specifications that complement the validation imposed by the types. These specifications are checked with an SMT solver. They can check for non-negative numbers, sorted lists, matching lengths of lists, membership of certain elements in a Set or Map, and more.