# LiquidHaskell is a GHC plugin that turns Haskell types into proof obligations

> A refinement type verification tool for Haskell, distributed on Hackage, that checks a program by handing its specifications to an SMT solver. The README spends more of its length on how to install and test it than on what it does, and that tells you where the friction is.

**ucsd-progsys/liquidhaskell** — Liquid Types For Haskell

- Repository: https://github.com/ucsd-progsys/liquidhaskell
- Stars: 1,336 · Forks: 166
- Language: Haskell
- License: BSD-3-Clause
- Published: 2026-10-19 · Updated: 2026-10-19 · Language: en
- Canonical page: https://hysenlabs.com/projects/ucsd-progsys-liquidhaskell

## The installation path is where the friction lives

LiquidHaskell is a formal verification tool for Haskell, and the README's first substantive sections are about getting it running rather than about what it verifies.

There are two documented routes. The Hackage route assumes the Z3 SMT solver version 4.15.1 or newer is installed and available in your PATH.

```
cabal install --lib liquidhaskell liquid-prelude liquid-vector --package-env . --force-reinstalls
ghc -fplugin=LiquidHaskell FILE.hs
```

The `--package-env .` flag matters and the README explains why. It creates a `.ghc.environment*` file in the current folder that makes ghc find the LiquidHaskell plugin only when invoking it from there, because otherwise global user configuration would be affected. That is a thoughtful default for a tool that installs a compiler plugin, since a plugin installed globally changes the behaviour of every compile you run.

There is a caveat attached to that route. The installation step is influenced by the dependencies that are already installed in your system, so different results may be obtained by different users. That is the sort of warning that appears when the tool's dependency footprint is large enough to interact with whatever is already on the machine.

The GitHub route pins the toolchain. The repository builds with GHC 9.14.1, cabal-install 3.16.1.0, and z3 4.15.1 or newer, all of which must be in your PATH.

```
git clone https://github.com/ucsd-progsys/liquidhaskell.git
cd liquidhaskell
git submodule update --init
cabal build liquidhaskell liquid-prelude liquid-vector

cabal exec -- ghc -fplugin=LiquidHaskell FILE.hs
```

The submodule step is there because the repository carries the specification libraries as submodules, and the `cabal exec` wrapper is what puts the freshly built plugin on the path for the compile.

One detail for anyone who is not a user. The README says this is the development site of the tool, and that if you are a user or just curious you probably want the documentation website instead. The two audiences are served by different artefacts, and a user should not be reading this repository's build instructions at all.

## The repository is a working system, not a single library

The top level directories describe the implementation, and the split tells you what the tool actually is.

There is `liquidhaskell-boot/`, which is the bootstrap library, and `liquid-fixpoint/`, which is the core verification engine. `liquid-prelude/` and `liquid-vector/` are the bundled specification libraries for common data structures, and `liquid-parallel/` handles the parallel solving. Then there are `liquid-finfield/` and the `nix-compat` style support directories.

The `liquidhaskell-boot` name is the interesting one, because it explains the architecture. A GHC plugin cannot be written in the language it checks without a bootstrap problem, so the boot library exists to break that cycle, and the development guide explains its consequence directly. When changing the `liquidhaskell-boot` library, sometimes you do not want to rebuild `liquidhaskell` or `liquid-vector` when testing the changes, and you can set the environment variable `LIQUID_DEV_MODE=true` when running `cabal` to skip rebuilding those packages. The README then adds a DANGER note, that this can give an invalid result if the changes to `liquidhaskell-boot` do require rebuilding other `liquid*` packages.

That is the cost of the design, stated plainly by the people who built it. A shortcut that is faster and sometimes wrong is documented as dangerous rather than quietly provided.

The other directories show the scope of the work. `docs/` holds the documentation including the mkDocs sources for options and specifications, `tests/` is the test suite, `benchmarks/` and `benchmark-timings/` are the performance infrastructure, `external/` and `files/` hold vendored material, and `nix-shells/` and `nixpkgs.nix` are the environment definitions. There is a `Syntax.md` describing the language extension, a `CHANGES.md`, a `Makefile`, and a `cabal.project`. The `LICENSE_Z3` file is worth noting, because it covers the bundled solver rather than the tool's own code.

## The test suite is a shell script and a cabal file, and you can swap the solver

The regression testing section is unusually concrete, and two of its features matter to anyone who wants to contribute or to measure.

All the tests run through a shell script.

```
$ ./scripts/test/test_plugin.sh
```

You can run a bunch of particular test groups instead by naming them, and you can list all the possible test options with `--help`, or get a list of just the test groups, one per line, with `--show-all`.

The second feature is more interesting. You can invoke cabal directly to pass in specific parameters.

```
$ cabal build tests:unit-neg --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination
```

And you can change the underlying solver.

```
$ cabal build tests:unit-pos --ghc-options=-fplugin-opt=LiquidHaskell:--smtsolver=cvc5
```

The solver is a plugin option, so the SMT backend is swappable. That matters for a verification tool, because different solvers have different performance characteristics on different kinds of quantifier patterns, and a project that hard-codes one solver cannot let you work around a pathological case. The `--no-termination` option in the first example is the same kind of escape hatch, a way to run the checks without the termination analysis.

You can also modify the number of used threads, depending on cores, and you can directly extend and run the tests by modifying the files in `tests/harness/`. Adding a test means picking a folder such as `tests/ple/pos`, adding a new file `MyTest.hs` with the test module, and then adding the module to the corresponding executable in `tests/tests.cabal`.

The parallelism story is one line. Tests run in parallel, unless the flag `--measure-timings` is specified to `test_plugin.sh`.

There is a Makefile as well, with the conventional Haskell targets. The `test` target is the one that shows the shape of a run.

```
test:
	$(CABAL) configure -fdevel --enable-tests --disable-library-profiling -O2
	$(CABAL) build
	$(CABAL) exec $(TASTY) -- --smtsolver $(SMTSOLVER) --hide-successes --rerun-update -p 'Unit/' -j$(THREADS) +RTS -N$(THREADS) -RTS
```

The `--smtsolver` variable defaults to `z3` at the top of the Makefile, `THREADS` defaults to 1, and the optimisation level switches between a fast `-O0` build and a distribution `-O2` one. The `--rerun-update` flag updates the expected outputs, which is how a test suite that checks proofs handles a change in the solver's output formatting.

## Performance measurement has its own pipeline, and a known pitfall

The section on performance comparison charts is a small case study in how to measure a compiler plugin, and the pitfall is stated first.

You must make sure to remove previous compilation artifacts of tests before measuring performance, or GHC will skip running Liquid Haskell on modules that do not need recompilation. The README notes that using `-fforce-recomp` is not ideal, with a pull request for the details, and gives the command that removes the artefacts instead.

```bash
find dist-newstyle -name "tests-*" -o -name "prover-ple-lib-*" | xargs rm -r
```

The mechanism is the important part. A verification plugin that runs as part of the compilation is invisible to the measurement when the compilation is cached, so the timings you collect are timings of nothing. That is a classic benchmarking trap and here it is called out in the README rather than discovered later.

The measurement itself is a flag.

```
$ ./scripts/test/test_plugin.sh --measure-timings
```

Measures are collected in `.dump-timings` files under the `dist-newstyle` directory, and it runs all tests and measures in parallel. The README is precise about the difference between the two flags. The `--measure-timings` flag is reliable if you want to measure allocations, but if you want to measure time and you want to reduce interference between the tests, you need the `--measure-timings-j1` flag instead, which runs tests one at a time.

That distinction is a well-judged one. Allocation counting is deterministic and can be done in parallel, whereas wall clock time in a parallel test run is measuring the contention as much as the work.

The collected files are then converted to JSON.

```bash
cabal build ghc-timings
cabal exec ghc-timings dist-newstyle
```

Which produces `tmp/*.json` files, and then a CSV report is generated from the JSON files with a benchmark target that takes a phase filter and an output path.

```bash
cabal run benchmark-timings -- tmp/*.json --phase LiquidHaskellCPU -o summary.csv
```

The phase filter is how you separate the CPU time of the verification from the other phases, and the `benchmark-timings/` directory in the repository holds that target.

## Version support is a moving target, and the releases say so

The recent releases are the clearest indicator of how the project is maintained, and each one is named for a compiler version rather than a feature.

v0.9.12.2.1 is the last version to build with GHC 9.12.2, published 2026-01-14. v0.9.12.2 is the first version to build with GHC 9.12.2, from 2025-03-22. v0.9.14.1 is a first version to build with GHC 9.14.1, from 2026-05-07.

So the project publishes a new version each time it moves to a new GHC, and the naming tells you the order. The tags are not a feature history, they are a compiler compatibility history, and the last two releases are within a year of each other with a GHC bump between them. The last push to the repository was on 2026-10-01 and the default branch is `develop`.

That pattern is what you would expect from a tool that is a compiler plugin. A GHC plugin is bound to the compiler's internal API, and every GHC release moves that API, so a new GHC means a new plugin release, which means the work between releases is maintenance rather than features.

The practical consequence for an adopter is that your GHC version determines your LiquidHaskell version, and the mapping is in the release names. There is a `README_MAINTAINERS.md` at the root for the maintainer-facing notes, a `TODO.md` and a `TODO.EASY.md` for the work queues, and a `proposals/` directory for design discussions. The `typeclass-tests/` and `liquid-finfield/` directories are for the typeclass and field handling, which are the two places where a refinement type system meets Haskell features that were not designed with it in mind.

The licence is BSD-3-Clause for the tool, with a separate `LICENSE_Z3` covering the bundled solver, and the support channels are a Zulip space, a Google Groups mailing list, the GitHub issue tracker, or email to Ranjit Jhala or Niki Vazou.

## Conclusion

Adopt LiquidHaskell if you are working in Haskell and want a machine-checked statement about a property that the type system cannot express, such as a value being positive or a list being sorted. Do not adopt it expecting the type system to change, since the checks are additional and separate from what GHC infers. Verify first that the solver version you have is one the tool is tested against, that the properties you want to state are expressible as refinements rather than as invariants, and that you are prepared for the checks to be slow on the properties that matter most.

## FAQ

### How do I install and run LiquidHaskell from Hackage?

You need the Z3 SMT solver at 4.15.1 or newer in your PATH, then run cabal install --lib liquidhaskell liquid-prelude liquid-vector --package-env . --force-reinstalls and compile with ghc -fplugin=LiquidHaskell FILE.hs. The --package-env . flag keeps the plugin out of your global ghc configuration.

### How do I build LiquidHaskell from the GitHub repository?

The repository builds with GHC 9.14.1, cabal-install 3.16.1.0 and z3 4.15.1 or newer, all in your PATH. Clone it, run git submodule update --init, then cabal build liquidhaskell liquid-prelude liquid-vector, and use cabal exec -- ghc -fplugin=LiquidHaskell FILE.hs to compile with the plugin.

### Can I use a different SMT solver with LiquidHaskell?

Yes. The solver is a plugin option, so cabal build tests:unit-pos --ghc-options=-fplugin-opt=LiquidHaskell:--smtsolver=cvc5 switches the backend for that run. The --no-termination option in the same form runs the checks without termination analysis.

### How do I run the LiquidHaskell regression tests?

Run ./scripts/test/test_plugin.sh for all of them, or pass test group names to run a subset. The --help flag lists the available options and --show-all lists the test groups one per line, and the underlying executable is documented in the README in the tests directory.

### How do I measure LiquidHaskell performance?

First remove previous compilation artefacts, find dist-newstyle -name "tests-*" -o -name "prover-ple-lib-*" | xargs rm -r, or GHC will skip modules that do not need recompilation and you will time nothing. Then run ./scripts/test/test_plugin.sh --measure-timings, and use --measure-timings-j1 instead if you want time rather than allocations, since it runs the tests one at a time.

## Sources

- [Issues](https://github.com/ucsd-progsys/liquidhaskell/issues)
- [License: BSD-3-Clause](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/LICENSE)
- [README](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/README.md)
- [Releases](https://github.com/ucsd-progsys/liquidhaskell/releases)
- [ucsd-progsys/liquidhaskell on GitHub](https://github.com/ucsd-progsys/liquidhaskell)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/ucsd-progsys-liquidhaskell