Does your program do what it is supposed to do?

OpenJML is a program verification tool for Java programs that allows you to check the specifications of programs annotated in the Java Modeling Language.

Download OpenJML

// Can you spot the two errors 
// in this program? 

public class MaybeAdd {
     //@ requires a > 0;
     //@ requires b > 0;
     //@ ensures \result == a+b;
     public static int add(int a, int b){
         return a-b;

    public static void main(String args[]){

Verify Your Java Programs with JML

The Java Modeling Language is a mature program specification language with over a decade of history. OpenJML is capable of checking Java programs annotated with specifications in the Java Modeling Language and provides robust support for many of JML's features.

The goal of the OpenJML project is to implement a full tool for JML and current Java that is easy for practioners and students to use to specify and verify Java programs. In addition, the project seeks to advance the theory and experience of software verification in practical, indsutrially-relevant contexts.

Learn more »

Support for Static and Runtime Checking

Verification in OpenJML can be performed either by using our extended static checking facilities or by using our runtime assertion checking features. Runtime assertion checking is often easier to write specifications for whereas static checking gives stronger guarantees about program behavior.

Learn more »

Integrates with Most Popular SMT Solvers

OpenJML is not a theorem prover or model checker itself. OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. OpenJML supports major SMT solvers such as Z3, CVC4 and Yices. The success of the proofs will depend on the capability of the SMT colver (e.g., which logics it supports), the particular logical encoding of the code+specifications, and the complexity and style in which the code and specifications are written.

Learn more »