VDMJ provides basic tool support for the VDM-SL, VDM++ and VDM-RT specification languages, written in Java. It includes a parser, a type checker, an interpreter (with arbitrary precision arithmetic), a debugger and a proof obligation generator as well as JUnit support for automatic testing and annotation support.VDMJ is a command line tool, but it is used by the Overture eclipse project, and the VDM VSCode extension which adds a full GUI interface.You can find the VDMJ project on GitHub. The original IPR for VDMJ is owned by my former employer, Fujitsu UK. The GitHub project is a derived work, under the GPL.

There is a one-page guide to using command line VDMJ here, and you can read the full User Guide here.

You can find out more about the VDM specification language here: