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.