Catch bugs before runtime with compile-time verification
LiquidJava adds refinement types and typestates to Java through annotations, enabling static verification that catches errors traditional type systems miss.
@Refinement("a > 0")
int a = 3; // ✓ verified safe
a = -8; // ✗ compile error- Refinement types - Express constraints beyond basic types
- Typestate verification - Track object state transitions
- SMT-backed - Powered by Z3 solver
- IDE integration - Real-time feedback in VS Code
- Lightweight - Annotation-based, works with existing Java code
📦 VS Code Extension
📚 Tutorial
💡 Examples
📖 Research Paper (ICSE 2023)
Learn more in the LiquidJava website.