Liquid Haskell

Liquid Haskell is a program verifier for the programming language Haskell which allows specifying correctness properties by using refinement types.^[1][2] Properties are verified using a satisfiability modulo theories (SMT) solver which is SMTLIB2-compliant, such as the Z3 Theorem Prover.

Liquid Haskell

Original author(s)	Niki Vazou, Eric Seidel Ranjit Jhala
Initial release	2014; 11 years ago (2014)
Stable release	0.9.2.5 / October 18, 2023; 19 months ago (2023-10-18)
Repository	github.com/ucsd-progsys/liquidhaskell
Written in	Haskell
Available in	English
Type	Formal program verifier
License	BSD 3-clause
Website	ucsd-progsys.github.io/liquidhaskell

See also

• Formal verification