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.
Verification Features
Understand how LiquidJava checks assignments, method calls, conditionals, and recursive methods.
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.
Playground
Try LiquidJava refinements and typestates directly in your browser.
Resources
Find LiquidJava papers, posters, and source repositories for deeper reading and experimentation.