Downloads

OpenJML is a tool for working with logical annotations in Java programs. It enables static or run-time checking of the validity of the annotations, with other features underway.

The tool is available as a standalone command-line application for MacOS and Linux (Ubuntu) and WSL on Windows and as a LSP-compliant server for various IDEs.

Installing OpenJML (Command Line Tool)

The OpenJML command line tool is OS-dependent. Download the appropriate release from the github latest release page.

The download retrieves a .zip file. Unzip the file into a new directory of your choice (call it $OJ). After unzipping, $OJ should contain the `openjml` executable and other files and folders. Some browsers or download utilities will automatically unzip the .zip file for you, leaving an unzipped folder in your downloads folder. You can move or rename the folder (with all its contents) to a location of your choice.

These are the particularly relevant files in the top-level of the installation folder:

  • openjml -- the javac-like tool that does (static) deductive verification, compiles a Java program with runtime assertion checks, and other functions.
  • openjml-java -- a build of Java (java-21-ga as of 2025) but with JML libraries included, helpful for running RAC-compiled Java programs
  • jmlruntime.jar -- the JML runtime files needed when executing Java files with runtime checks compiled in
  • OpenJMLUserGuide.pdf -- a copy of the reference manual for the OpenJML tool
  • JML_Reference_Manual.pdf -- a copy of the JML (language) reference manual
  • openjml-compile -- this script compiles a Java program that uses openjml capabilities programmatically
  • openjml-run -- this script runs a program compiled by openjml-compile
  • openjml-lsp -- an executable script that launches a LSP-compliant server (for use by client IDEs)

Current versions of the pdf documentation files are also available from this web site.

If $OJ is the installation directory, then you can run openjml using the command line $OJ/openjml. For example, $OJ/openjml --version will emit the version number of its build.

Further instructions about running OpenJML can be found in the tutorial.

Language Server and IDEs

OpenJML also has extensions to various IDEs, implemented using a LSP-compliant wrapper around the OpenJML command-line tool. These IDE extensions require an installation of OpenJML to function.
  • A VSCode extension is part of the OpenJML download.
  • An Eclipse plugin can be installed from OpenJML's Eclipse update site at openjml.org/eclipse-update-site

SMT solvers

OpenJML uses SMT solvers as logic checkers. A selection of supported solvers is bundled with the OpenJML release.