JmlGen generates JML annotations from what can be guessed out of a java project: the result, a JML-annotated project, can then be processed by JML tools, like the OpenJml program verification tool. Check the current functions offered and try them on your own java software.
For more instructions, please read the full beta-testing campaign