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

1. 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.
2. Java 17. Required by the subprojects library, common, and javac-plugin.
3. Lean 4 (via elan) — needed to build the Strata verification back-end.
4. cvc5 SMT solver on your PATH.
5. z3 SMT solver (v4.15.2 recommended) on your PATH.

Building

1. Check out the JVerify repository and its submodules:

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

2. Navigate to the JVerify repository directory.
3. Build the verifier CLI:

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

4. Build the Strata back-end. The strata command-line executable lives in the StrataCLI sub-package, so build from there (this also builds the Strata library it depends on):

   cd Strata/StrataCLI && lake build && cd ../..
   

5. 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). This is the Strata repository root, not the StrataCLI sub-directory — JVerify locates the strata executable under StrataCLI itself.

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.

Related open issues

• 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;
        }
    }
}

Testing unverified contracts

If proving that a JVerify method matches its specification is difficult, then you can choose to instead test it using property-based testing. This is generally more compute heavy, and is therefore best suited for pieces of code near the bottom of the call-stack. Although it does not require a proof, it does require that the programmer specifies how to generate inputs for the method to test. JVerify supports the generator annotations from the Java property based testing tool jqwik.

Marking a contract for testing

Annotate the method whose contract you want to test with @AsProperty, and annotate its parameters with jqwik’s @ForAll so that jqwik knows to generate values for them. The pre- and postconditions are written as method calls in the body.

import org.strata.jverify.AsProperty;
import org.strata.jverify.Pure;
import net.jqwik.api.ForAll;

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

@AsProperty
@Pure
int abs(@ForAll int x) {
    precondition(x != Integer.MIN_VALUE);
    postcondition((Integer r) -> r >= 0 && (r == x || r == -x));
    return x < 0 ? -x : x;
}

The postcondition is a genuine property — the result is non-negative and has the same magnitude as the input — not merely a restatement of the one-line body. The precondition excludes Integer.MIN_VALUE, whose negation overflows (-Integer.MIN_VALUE == Integer.MIN_VALUE, which is negative); without it the property would fail on exactly that input, which is the kind of edge case property-based testing is good at finding.

Contracts under test must be executable. Unlike a contract you verify, a contract you test is actually run, so its pre- and postconditions must be ordinary executable Java. Verification-only constructs — forall, exists, sequence, and similar — have no runtime behaviour (they throw if executed), so the tool skips clauses containing forall/exists and you should express testable properties in plain Java instead.

Why @Pure? A generated property test checks the postcondition but never the frame, so dropping a modifies clause is only provably sound when the method is @Pure or its frame is modifies(everything()) (see Frame clauses and soundness). abs modifies nothing and has no loop, so we mark it @Pure; JVerify then guarantees it is side-effect-free, which is what makes testing its postcondition sound and keeps the translation warning-free.

Generating the jqwik property

The contracts2jqwik tool translates an @AsProperty method into a jqwik @Property test. It is a source-to-source generator: you give it a .java file and it produces a sibling .java file containing the property tests, which you review and check in alongside the original.

Build the tool’s runnable distribution from the JVerify repository root:

./gradlew :contracts2jqwik:installDist

Then run it on a file. With one argument it writes the generated source to stdout:

./contracts2jqwik/build/install/contracts2jqwik/bin/contracts2jqwik path/to/Foo.java

With a second argument it writes the generated source to disk:

./contracts2jqwik/build/install/contracts2jqwik/bin/contracts2jqwik path/to/Foo.java path/to/FooGenerated.java

If the input declares a class Foo, the generated output declares a class FooGenerated that extends Foo, so the generated tests can call the contract methods (and any @Provide generators) directly. The tool processes one file at a time; wiring it into a larger Gradle pipeline that runs over a whole source set is left to the consumer’s build.

Worked example

Assuming the abs method above lives in a class AbsProperty, running the tool on that file produces:

package org.strata.jverify.examples;

import net.jqwik.api.Assume;
import net.jqwik.api.ForAll;
import net.jqwik.api.Property;
// ... (the original imports are carried forward)

public class AbsPropertyGenerated extends AbsProperty {

    @Property
    public boolean absProperty(@ForAll int x) {
        Assume.that(x != Integer.MIN_VALUE);
        int r = abs(x);
        return (r >= 0 && (r == x || r == -x));
    }
}

jqwik then generates values for x, discards the (single) value that fails the Assume.that(...) precondition, and checks that the postcondition holds for the rest.

Advanced: expensive preconditions and custom generators

The abs precondition excludes just one value, so rejection sampling is free. But some preconditions are satisfied by almost none of the randomly-generated inputs. Consider a binary search, whose precondition is that the array is sorted:

@AsProperty
int binarySearch(@ForAll int[] arr, @ForAll int target) {
    precondition(isSorted(arr));
    postcondition((Integer r) -> contains(arr, target)
        ? 0 <= r && r < arr.length && arr[r] == target
        : r == -1);
    // ... iterative binary search ...
}

A randomly-generated array is almost never sorted (the probability is 1/n!), so a @Property that relied on Assume.that(isSorted(arr)) would discard nearly every input. jqwik aborts a property whose discard ratio is too high, so this would not just be slow — it would fail to run at all.

The fix is to generate valid inputs directly rather than filter random ones. jqwik does this with a @Provide method referenced by name from @ForAll:

@Provide
Arbitrary<int[]> sortedArrays() {
    return Arbitraries.integers().between(-50, 50)
        .array(int[].class).ofMaxSize(16)
        .map(a -> { java.util.Arrays.sort(a); return a; });   // generate, then sort
}

Annotate the parameter with the generator’s name, @ForAll("sortedArrays") int[] arr; contracts2jqwik carries that annotation through to the generated @Property. Now every generated array is already sorted, the Assume.that(isSorted(arr)) is always satisfied, and nothing is discarded.

When a contract method cannot be @Pure

binarySearch uses a loop, so it cannot be @Pure (pure methods may not loop or reassign variables). It still modifies no objects, but contracts2jqwik cannot confirm that, so it translates the method and prints a frame soundness warning recording that the generated test does not check the frame (see Frame clauses and soundness). Since the method is frame-clean by inspection, the warning is the only signal you need — the property runs as usual:

contracts2jqwik path/to/BinarySearchProperty.java

Translation rules

The translation is otherwise verbatim: clauses are emitted as written, except that each conjunct is parenthesised when several postconditions are joined with &&.

Time-traveling with old(...)

old(e) lets a postcondition refer to the pre-call value of an expression. The tool makes this executable by snapshotting e into a temporary before the method runs, then substituting that temporary back into the postcondition. For example:

@AsProperty
@Pure
public static int increment(@ForAll int n) {
    postcondition((Integer r) -> r == old(n) + 1);
    return n + 1;
}

generates:

@Property
public boolean incrementProperty(@ForAll int n) {
    var __old0 = n;
    int r = increment(n);
    return (r == __old0 + 1);
}

This works as long as the expression inside old(...) refers only to the contract method’s parameters. If it refers to a local declared inside the contract body (for example a receiver constructed there), the snapshot can’t be formed in the generated test, so that clause is skipped with a warning rather than emitting broken code. Supporting old(...) over a constructed receiver requires generating the receiver too, which is not yet implemented.

Frame clauses and soundness

A modifies(...) clause is a promise about which objects a method may mutate (see Reading and modifying objects). The verifier checks that promise, but a generated property test only evaluates the postcondition — it never observes which objects the method touched. So simply dropping the modifies clause would be unsound: a method that mutates more than its frame allows would still pass the generated test, even though verification would reject it. Testing a contract is meant to be a weaker but sound stand-in for verifying it, and silently ignoring the frame breaks that.

To make this explicit, contracts2jqwik always translates the method (the frame is dropped either way), but it stays silent only when dropping the frame loses nothing — that is, when either:

• the method is @Pure — JVerify independently guarantees a pure method modifies nothing, so there is no frame obligation left for the test to check; or
• its frame is exactly modifies(everything()) — an unconstraining frame with nothing to violate.

For any other method it translates but emits a frame soundness warning:

• a non-@Pure method with a narrower modifies(...) clause, or
• a non-@Pure method with no modifies clause — JVerify’s default frame is empty (the method may modify nothing), which is itself a promise the test cannot check.

The warning records that the generated test does not check the frame, so the result is only guaranteed sound when the method is @Pure or its frame is modifies(everything()). If a method genuinely mutates nothing, mark it @Pure (as abs is above) to silence the warning. If it cannot be @Pure but you can see it is frame-clean — like the looping binarySearch above — the warning is just a reminder; the property still runs.

A fully sound treatment of arbitrary frames would require checking the modifies clause at runtime (instrumenting each field write in the method, and propagating each callee’s frame into its caller’s). That is not yet implemented; the warning marks exactly where that gap remains.

reads(...) clauses, by contrast, constrain only what a @Pure method may read and have no runtime effect, so they are simply dropped.

Warnings for skipped clauses and methods are printed to stderr so you can see exactly what was and wasn’t translated.