Extending Java with Liquid Types

LiquidJava is an additional type system for Java that uses liquid types to express constraints programs must follow, helping catch more bugs before they run.

Getting Started

Set up your environment and run your first LiquidJava verification.

Annotations

Learn the different annotations in LiquidJava for writing specifications.

Diagnostics

Learn about the different types of errors and warnings, how to use custom error messages, and how to interpret refinement errors.

VS Code Extension

Use the LiquidJava VS Code extension for live diagnostics, syntax highlighting, and IDE feedback while editing Java code.

Command-Line Interface

Run the LiquidJava verifier from the command line for local checks, debugging, and CI workflows.

Examples

LiquidJava example usages with focused code snippets.

Resources

Find LiquidJava papers, posters, and source repositories for deeper reading and experimentation.