Liquid Haskell

{{Infobox software

| title = Liquid Haskell

| logo =

| logo caption =

| logo alt =

| logo size =

| screenshot =

| screenshot size =

| screenshot alt =

| caption =

| author = Niki Vazou, Eric Seidel
Ranjit Jhala

| developer =

| released = {{Start date and age|2014}}

| latest release version = 0.9.2.5

| latest release date = {{Start date and age|2023|10|18}}

| repo = {{URL|github.com/ucsd-progsys/liquidhaskell}}

| programming language = Haskell

| operating system =

| platform =

| size =

| language = English

| genre = Formal program verifier

| license = BSD 3-clause

| website = {{URL|ucsd-progsys.github.io/liquidhaskell}}

| AsOf =

}}

Liquid Haskell is a program verifier for the programming language Haskell which allows specifying correctness properties by using refinement types.{{cite thesis |last=Vazou |first=Niki |title=Liquid Haskell: Haskell as a theorem prover |publisher=University of California |date=2016}}{{cite conference |last1=Vazou |first1=Niki |last2=Seidel |first2=Eric |date=2014 |url=https://dl.acm.org/citation.cfm?id=2628161 |title=Refinement types for Haskell |publisher=ACM |book-title=Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming |pages=269–282 |conference=International Conference on Functional Programming |doi=10.1145/2692915.2628161|url-access=subscription }} Properties are verified using a satisfiability modulo theories (SMT) solver which is SMTLIB2-compliant, such as the Z3 Theorem Prover.