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 and its tools here: