LiquidHaskell is a formal verification tool for Haskell. It extends Haskell’s type system with refinement types, allowing programmers to express properties about values and have those properties checked automatically.
A normal Haskell type might state that a function accepts and returns an integer. A refinement type can place additional constraints on those values. This makes it possible to state conditions such as a number being positive, an index remaining within bounds or a function returning a value that satisfies a particular relationship with its input.
LiquidHaskell translates these specifications into logical constraints and uses an SMT solver to determine whether the program satisfies them. This lets it detect classes of errors that are outside the scope of the standard Haskell type checker while retaining a workflow that is closely integrated with Haskell source code.
The software can operate as a GHC plugin. This means verification can be incorporated into the compilation workflow instead of requiring a completely separate language or toolchain. Specifications are normally placed alongside the Haskell code they describe.
LiquidHaskell is more than a conventional source-code linter. Its emphasis is proving properties about programs rather than checking formatting or stylistic conventions. Nevertheless, it occupies a useful place in a Haskell static-analysis toolkit because it can highlight invalid assumptions and unsafe program states before the code is run.
It uses Z3 for SMT solving and is suitable for developers interested in stronger static guarantees than Haskell’s standard type system provides.
This is free and open source software.
Key Features
- Adds refinement types to Haskell programs.
- Checks program properties using SMT solving.
- Integrates with GHC as a compiler plugin.
- Allows specifications to be written alongside Haskell source code.
- Can verify relationships between function inputs and outputs.
- Helps detect invalid program states through static verification.
- Uses Z3 as its SMT solver.
Website: github.com/ucsd-progsys/liquidhaskell
Support:
Developer: UCSD Programming Systems Group
License: BSD 3-Clause “New” or “Revised” License
LiquidHaskell is written in Haskell. Learn Haskell with our recommended free books and free tutorials.
Related Software
| Haskell Linters | |
|---|---|
| Ormolu | Formatter for Haskell source code |
| HLint | Suggests improvements to Haskell code |
| Fourmolu | Formatter for Haskell source code, fork of Ormolu |
| stylish-haskell | Simple Haskell code prettifier |
| hindent | Extensible Haskell pretty printer |
| Stan | Haskell STatic ANalyser |
| Floskell | Flexible Haskell source code pretty printer |
| Weeder | Perform whole-program dead-code analysis |
Read our verdict in the software roundup.
 Explore our carefully curated directory of recommended free and open source software, covering every major software category.The directory forms part of our extensive collection of articles for Linux enthusiasts. It includes hundreds of detailed reviews, together with free and open source alternatives to proprietary software from companies such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. LinuxLinks also covers interesting projects worth exploring, Linux-compatible hardware, free programming books and tutorials, and much more. Know a useful free and open source Linux application that we haven’t covered? Tell us about it using our submission form. |
Please read our Comment Policy before commenting.