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, Cygwin and CMD on Windows and as a LSP-compliant server for various IDEs. Use Linux distributions for WSL and Windows distributions for Cygwin.

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. Use the scripts with a .bat extension on WIndows and in Cygwin; use the scripts without an extension on Linux and MacOS.

  • openjml(.bat) -- the javac-like tool that does (static) deductive verification, compiles a Java program with runtime assertion checks, and other functions.
  • openjml-java(.bat) -- 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(.bat) -- this script compiles a Java program that uses openjml capabilities programmatically
  • openjml-run(.bat) -- this script runs a program compiled by openjml-compile
  • openjml-lsp -- an executable script that launches a LSP-compliant server (for internal 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.