Overture Tool
Formal Modelling in VDM
VDM Tools
“Validated Designs for Object-oriented Systems” is supported by high quality industry-strength tools that previously was owned and marketed by CSK Systems Corporation of Japan. The full functionality includes model syntax- and type-checking, an interpreter, test coverage support, proof obligation generation, code generation for C++ and Java, the link to Rose, and much more. Platforms supported include Linux, Windows, MacOS. It has now been turned into open-source software.
VDMTools is a fully featured toolbox for VDM-family with a long history. It has both IDE with GUI and command line tools with features including syntax checkers, type checkers, interpreters, proof obligation generators and code generators. Binary packages (for Mac, Linux and Widnows) and documentation (in English and Japanese) are available at fmvdm site, and all source code and documentation are now open-sourced under GPLv3 at github repository.