JML Home Page

About JML

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus.

The draft paper Design by Contract with JML (by Gary T. Leavens and Yoonsik Cheon) explains the most basic use of JML as a design by contract (DBC) language for Java.

The papers below describe JML very briefly and some of its tools. The paper Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 (by Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll) contains a description of JML and its tools that is suitable for those who are already more familiar with the idea of assertions. The second gives a summary of all known tools.


From the download page you can choose between several open-source tools for using JML. The most useful of these are an assertion-checking compiler (jmlc), a unit testing tool (jmlunit), and an enhanced version of javadoc (jmldoc) that understands JML specifications. See the papers above and the documentation for details.

In March 2022, JML received a "Community Choice Award" which recognized JML having over 10,000 downloads. (This is a bit ironic, as development of JML's tools has moved to, although it started out on


The work on JML is a cooperative effort between:

JML is an open project, and we welcome the participation of other groups. If your group is working on JML but not listed above, please send an email to Gary Leavens (

Development of JML is hosted on

Last modified Wednesday, March 2, 2022.