NOTE: This site is archived content and is, for the most part, no longer being actively updated. Information on a permanent new home for JMLUnitNG will be available soon; the most recent version released before this site was archived will continue to be available here.


  • JMLUnitNG - unit test generator for JML-annotated Java classes, including those written in modern (1.5 and later) Java dialects
  • OpenJML on Mac OS X