Liquid Haskell allows to annotate code with specificationsthat 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 aSet orMap, andmore.