JVerify

Current status: JVerify is under active development and currently supports a limited subset of Java. It is built on Strata. Some examples in this guide use features that don’t verify yet — treat them as illustrations of intended behavior. See Supported Java features and issue #384 for details.

JVerify is a tool that helps ensure the correctness of Java programs. There are many existing tools for this. However, such tools are often either incomplete, not revealing bugs that are present, or inaccurate, reporting a problem when there is no bug.

JVerify is both complete and accurate. JVerify is complete because it allows the programmer to specify any type of behavior for their program, after which JVerify can ensure the implementation matches this. Typically desired behaviors, such as that the program does not throw any uncaught exceptions, or that the program must eventually terminate, do not need to be specified since JVerify knows about them already.

JVerify is accurate because when it is not sure that the program behaves according to a particular specification, it allows the programmer to provide hints, enabling it to decide whether there is a bug or not.

The specifications and hints used by JVerify are added to the program using regular Java calls to the JVerify library, enabling existing IDEs to be used.

To see examples of bugs that JVerify can detect, have a look at this section.

Frequently asked questions

Should I use JVerify in production right now?

No, JVerify is not yet ready for production use. The user experience, amount of support for the Java language and reliability is not yet at the level that we think it is likely to give you a good experience.

However, you can use the installation and Running JVerify sections in this guide to explore what it can currently do.

Does JVerify support the entire Java language?

Not yet, but it will support all Java language features. Note that we differentiate between Java the language, as documented in its specification, and the Java standard library. More on JVerify’s support for the latter is further down this FAQ.

Despite JVerify supporting all Java language features, there may be edge-cases where despite sufficient verification hints by the programmer, JVerify can not prove the correctness of a correct program. In these cases, you can either skip verification, or otherwise you will have to modify the program, even though it’s already correct. One class of these edge-cases is where verification depends on information from the type system, and needs a downcast where the type system does not require one.

You can find the list of currently supported Java features here: supported Java features, together with the known cases where JVerify can not verify a valid programs.

Can I gradually adopt JVerify in an existing codebase?

Yes, more about that is in partially verifying a codebase.

Can I use JVerify when calling libraries that were developed without JVerify?

Yes, more about that is in adding contracts to third-party code. For the Java standard library, JVerify provides contracts for the most commonly used part of it out of the box. It will support most types from java.lang, java.math and java.util. You can find which part of the standard library is currently supported in the section supported Java features.

Which IDEs can I use with JVerify?

You can use any Java IDE when working with JVerify.

Will adding calls to the JVerify library slow down the execution of my program?

No, more about that is in erasing verification code during compilation.

Can JVerify prove that code has a bug?

No, currently JVerify can only prove the absence of bugs, but it can not prove their presence. If JVerify returns an error, this may be because of an actual bug or because it needs more proof hints.

This guide

This guide assumes that you’re already familiar with Java. Specifications used by JVerify are written using regular Java expressions. However, verifying the correctness of Java code uses concepts that do not exist in regular Java, such as pre- and post-conditions. You can view JVerify as extending the Java language, even though it does not introduce any new syntax. This guide will walk you through the concepts that JVerify introduces.

JVerify uses a tool called a Satisfiability Modulo Theories (SMT) solver to help prove program correctness. Using this tool, JVerify will intelligently search through a space of proofs. For simple proofs, it can find them without help. For more complex proofs however, JVerify needs hints from you, the programmer. This guide will help you understand when JVerify does or does not need hints, and how to provide those.

Installation

JVerify can currently only be used by building it from source.

Prerequisites

Java 23. If you have a different default Java version installed, pass -Dorg.gradle.java.home=path-to-java-23 to the gradle commands below.
Lean 4 (via elan) — needed to build the Strata verification back-end.
cvc5 SMT solver on your PATH.

Building

Check out the JVerify repository and its submodules:

git clone https://github.com/strata-org/jverify.git --recurse-submodules

Navigate to the JVerify repository directory.

Build the verifier CLI:

./gradlew installDist     # macOS / Linux
./gradlew.bat installDist # Windows

Build the Strata back-end:
```
cd Strata && lake build && cd ..
```
Point JVerify at the Strata project directory by setting the JVERIFY_STRATA environment variable:
```
export JVERIFY_STRATA=$(pwd)/Strata
```
(or pass --strata /path/to/Strata on every JVerify invocation).

Running JVerify

Let’s try running JVerify on the following Java program, found here:

package org.strata.jverify.examples;

import static org.strata.jverify.JVerify.*;

class GaussianSum {
    /**
     * Returns 0 + 1 + 2 + ... + n.
     *
     * JVerify proves that the result equals the closed form n * (n + 1) / 2
     * for every n in [0, 65535]. The proof relies on two loop invariants:
     * a bound on the loop counter, and a closed-form relation that holds at
     * every iteration.
     */
    static int sumTo(int n) {
        precondition(0 <= n && n <= 65535);
        postcondition((int res) -> res == n * (n + 1) / 2);
        int i = 0;
        int s = 0;
        while (i < n) {
            invariant(0 <= i && i <= n);
            invariant(s == i * (i + 1) / 2);
            i = i + 1;
            s = s + i;
        }
        return s;
    }
}

sumTo(n) claims it returns the closed form n * (n + 1) / 2. JVerify checks that claim against the actual loop using two invariants: one bounds the loop counter, the other ties the running sum to the closed form.

To run JVerify, from the repository root:

./verifier/build/install/verifier/bin/verifier ./examples/src/test/java/org/strata/jverify/examples/GaussianSum.java

or on Windows:

./verifier/build/install/verifier/bin/verifier.bat ./examples/src/test/java/org/strata/jverify/examples/GaussianSum.java

You should see the following output:

Found 0 errors
Verified methods: 2
Failed methods: 0
Skipped methods: 0

If the JVERIFY_STRATA environment variable is not set, pass the Strata project directory explicitly with --strata ./Strata.

Try editing GaussianSum.java to introduce a bug — for example, change return s; to return s + 1; — and re-run. JVerify reports:

GaussianSum.java(16:36-16:58): Error: assertion could not be proved
Found 1 errors
Verified methods: 1
Failed methods: 1
Skipped methods: 0

The line and column point at the failing postcondition.

Adding JVerify to a Java project

To verify your own code, add the JVerify library as a compile-time dependency so you can use annotations such as @Pure and specification methods such as precondition. In a Gradle build script:

dependencies {
    implementation("org.strata.jverify:library:1.0-SNAPSHOT")
    // ...
}

Because the JVerify packages are not yet published to any shared repositories, run ./gradlew publishToMavenLocal first so this can be resolved. See the sample project for more details.

Current limitations

JVerify currently supports a limited subset of Java. See Supported Java features and issue #384 for the current state.

Let the number of reported verified things match Java concepts: #127
Support showing diagnostics using snippets: #128
Support running verification from the annotation processor as well: #159
Avoid needing to add --add-export when using the javac-plugin: #160

Supported Java features

JVerify intends to support the full Java language, but is actively under development. It is built on Strata and currently supports a limited subset of Java. Support is being expanded incrementally — see issue #384 for the roadmap.

Currently supported

Static methods only. Instance methods are silently skipped.
Primitive integer types: byte, short, int, long.
Boolean type.
Arithmetic, comparison, logical operators.
Ternary expressions.
Control flow: if/else, while, for, return, assert, variable declarations, blocks.
JVerify contract primitives: precondition(), postcondition(), check(), assume(), implies(), invariant().
Quantifiers: forall(), exists().
Pure static methods via @Pure.
Static method calls.

Not yet supported

Major gaps being actively worked on or planned:

Instance methods, constructors, fields, this
Reference types: classes, interfaces, records
Arrays
Generics / type parameters
float, double, char, String
Boxed primitive types (Integer, Long, …)
JVerify annotations: @Nullable, @Unbounded, @Nat, @Contract, @InheritContract, @Impure, @Invariant
old() in postconditions
Inheritance, interfaces, abstract classes
Lambdas (beyond contract lambdas)
break, continue, switch statements/expressions, throw
Bitwise and shift operators
Compound assignment (+=), increment/decrement (++, --)
Java standard library support (collections, BigInteger, streams, optionals)

If you encounter something not in either list, please open a GitHub issue.

Loop Invariants

JVerify verifies the behavior of code with loops through the use of a loop invariant. Since JVerify does not know how often a loop iterates, it needs to work with information that is true for any iteration. The loop invariant is a condition that must be true every time the loop guard is evaluated, so when the loop is first entered, and after each execution of the body.

The loop invariant can be used both to know what is true inside the loop, useful to prove the absence of exceptions inside it, and to learn about the state of the program when the loop exits.

Here follows the binary search example from the last section, but with some loop invariants added. Using the invariants, JVerify no longer emits an error about the array access inside the loop.

class BinarySearch {
    int binarySearch(int[] arr, int target) {
        var lo = 1;
        var hi = arr.length;

        while (lo < hi) {
            invariant(0 <= lo);
            invariant(lo <= hi);
            invariant(hi <= arr.length);

            var mid = lo + (hi - lo) / 2;
            if (key < arr[mid]) {
                hi = mid;
            } else if (arr[mid] < key) {
                lo = mid + 1;
            } else {
                return mid;
            }
        }
        return -1;
    }
}

If we would now introduce a bug, for example by replacing

var hi = arr.length;

with

var hi = arr.length - 1;

Then JVerify emits the error:

error: this invariant could not be proved on entry
 | invariant(lo <= hi);
             ^^^^^^^^

In this section, we’ve used invariants to prove that no uncaught exceptions occur inside the loop.

In the next sections, Pre- and post-conditions, Code types, Forall and exists, we will introduce the tools needed to prove the correctness of the above binarySearch example, and we will also use invariants to prove facts that hold after the loop exits.

Preconditions and postconditions

Besides detecting exceptions, JVerify allows you to precisely state what a method does, and check that it actually does that. We can prove that the binary search method shown in the previous section behaves as intended by giving it a contract, which is done using calls to precondition and postcondition.

Below we show the updated example. The added call to postcondition guarantees that the method behaves as intended. We had to add a call to precondition to be able to prove the postcondition, which also has the desired effect of preventing us from incorrectly calling binarySearch. The method only behaves as intended if called with a sorted list, and this is now checked by JVerify because of the precondition, as you can see here:

  void callBinarySearch() {
    binarySearch(new int[] {4, 1, 5}, 1);
//              ^ error: could not prove precondition
    binarySearch(new int[] {1, 3, 5}, 1); // no error
  }

Note that the updated example contains calls to several JVerify utility methods that we have not seen before: sequence, contains, drop and take. sequence converts an array to a JVerify type Sequence which is similar to an immutable Java List, and is useful for verification. On a Sequence we can call contains,take and drop, which behave as you’d expect from these common methods.

Lastly, we’re calling the JVerify method forall. We’ll cover how this works in the section Quantifiers later on. In the below example, the comments explain what it means there.

class BinarySearch {    
  int binarySearch(int[] arr, int target) {
    // This postcondition guarantees that the method behaves as desired
    postcondition((Integer r) -> sequence(arr).contains(target)
      ? 0 <= r && r < arr.length && arr[r] == target
      : r == -1
    );

    // The following precondition states that the input arr must be sorted.
    // Without this, we won't be able to prove the two new loop invariants, 
    // which are needed to prove the postcondition.
    // The method `forall` is one we'll get back to in the section Quantifiers
    precondition(forall((Integer i, Integer j) ->
            implies(0 <= i && i < j && j < arr.length, arr[i] < arr[j])));
    
    // implementation
    var left = 0;
    var right = arr.length - 1;
    
    while (left < right) 
    {
      invariant(0 <= left);
      invariant(left <= right);
      invariant(right <= arr.length);
      invariant(!sequence(arr).drop(left).contains(target)); // added
      invariant(!sequence(arr).take(right).contains(target)); // added

      var mid = (left + right) / 2;
      if (arr[mid] == target) {
          // JVerify can prove sequence(arr).contains(target)
          // and 0 <= mid && mid < arr.length && arr[mid] == target
          return mid;
      }
      if (arr[mid] < target) {
          left = mid + 1; 
          // JVerify uses the preconditon to prove the 4th invariant
      } else {
          right = mid; 
          // JVerify uses the precondition to prove the 5th invariant
      }
    }
    // JVerify uses the 4th and 5th invariant to prove that !sequence(arr).contains(target)
    return -1;
  }
}

If we now change anything in the implementation of binarySearch that would change its meaning, JVerify detects that the implementation no longer matches the specification and emits an error.

In the next section, Code types, we’ll improve the code by extracting the sorted predicate from the precondition into a separate method, so it’s self-documenting and reusable.

Quantifiers

JVerify introduces a special kind of expression called a quantifier. There are two types of quantifiers, forall and exists. Both take a lambda that can take any number of arguments of any type. The forall states that for all inputs the lambda could possibly take, the lambda body must be true, and the exists states that there must exist an input to the lambda for which the body is true.

Given a forall that ranges over types with infinitely many values, such as all integers, we can only ever determine if the forall holds by using logical reasoning. Similar, for an exists expression with an infinite domain, we can only prove that it is false by using logical reasoning. For these reasons, these types of expression do not occur in regular Java. forall and exists can only be used in an erased context, since these can not be executed at runtime.

You can use quantifiers to say something about the behavior of methods. For example, given an argument of type Function, we can say that this function only returns values greater than 10:

void higherOrder(f: Function<Integer, Integer>) {
  precondition(forall((Integer i) -> f(i) > 10);
}

Or that a List only contains even values

void higherOrder(l: List<Integer>) {
  precondition(forall((Integer i) -> l.get(i) % 2 == 0);
}

In the next section, Code purposes, we’ll reflect on what we’ve seen so far by introducing terminology that allows us to talk about the different usages of code when working with JVerify.

Integers

This section explain how prove properties about integers in Java code.

Nat

The annotation @Nat can be used to tell JVerify that an integer is never negative. Example:

int factorial(@Nat int n) {
    if (n == 0) {
        return 1;
    } else {
        return factorial(n - 1); // pass
    }
}

Without the @Nat annotation, JVerify would not have been able to prove termination, and indeed the program does not terminate if n is smaller than zero. Instead of @Nat, we could also have used precondition(n >= 0), but that is more verbose.

Bounded numbers

The types byte, int, short and long in Java are bounded. The values of these numbers all have lower and upper bounds, and doing arithmetic operations that cause these numbers to surpass these bounds, called an overflow, generally causes undesired results.

JVerify will check that any arithmetic operations on bounded numbers will not overflow. Example:

int triple(int x) {
  return 3 * x; // error: returned value may not be within the bounds of 'int'    
}

You can let JVerify know no such overflow occurs by bounding the provided values:

int triple(int x) {
  precondition(3 * x < Integer.MAX_VALUE);
  
  return 3 * x; // pass    
}

Unbounded numbers

Using the annotation @Unbounded, you can annotate integer types so JVerify will allow them to have unbounded values. Example:

@Erased
@Unbounded int triple(int x) {
  return 3 * x; // pass    
}

Note that the @Unbounded annotation can only be used in erased code. It is often useful in specifications, because working with unbounded numbers is easier, and since specifications are erased, they can use them.

Combining the above

Here follows an example that uses unbounded numbers is its specification, bounded numbers in the implementation, and natural numbers in both. It shows how each of these concepts is useful:

package org.strata.jverify.examples;

import static org.strata.jverify.JVerify.*;
import org.strata.jverify.*;

class Fibonacci {
    @Pure
    @Erased
    static @Unbounded @Nat int spec(@Unbounded @Nat int n) {
        return n < 2 ? n : spec(n - 1) + spec(n - 2);
    }

    public static @Nat int implementation(@Nat int n)
    {
        postcondition((int result) -> result == spec(n));
        
        // this precondition prevents overflow later in this method
        precondition(spec(n) <= Integer.MAX_VALUE);

        if (n == 0) {
            return 0;
        }

        int previousResult = 0;
        int result = 1;
        int i = 1;
        while(i < n)
        {
            invariant(result == spec(i));
            invariant(previousResult == spec(i - 1));
            invariant(i <= n);

            i = i + 1;

            // Using the precondition that the final result fits in an int32
            // And the knowledge that the intermediate results are smaller than the result
            // We can show the addition always fits in an int32
            SpecIsIncreasing(i, n);
            int addition = result + previousResult;
            previousResult = result;
            result = addition;
        }
        return result;
    }

    /**
     * Proves that Fibonacci numbers increase in value with increading input value
     */
    @Erased
    static void SpecIsIncreasing(@Unbounded @Nat int i, @Unbounded @Nat int j)
    {
        precondition(i <= j);
        postcondition(spec(i) <= spec(j));

        @Unbounded @Nat int x = i;
        while(x < j)
        {
            invariant(x <= j);
            invariant(spec(i) <= spec(x));
            x = x + 1;
        }
    }
}

Keyboard shortcuts

JVerify User Guide