jCUTE     http://osl.cs.uiuc.edu/~ksen/cute/

Microsoft's SLAM  http://research.microsoft.com/en-us/projects/slam/

Sireum/Kiasan for Java  http://www.sireum.org/?q=node/21 

Java Pathfinder   http://javapathfinder.sourceforge.net/  

Java Modeling Language (JML) http://www.cs.ucf.edu/~leavens/JML/  

Extended Static Checker for Java http://kind.ucd.ie/products/opensource/ESCJava2/  

Bandera http://bandera.projects.cis.ksu.edu/  

Labelled Transition Analyzer (LTSA) http://www.doc.ic.ac.uk/ltsa/eclipse/  

Daikon invariant detector http://groups.csail.mit.edu/pag/daikon/download/  

FDR2 http://www.fsel.com/software.html

ACL2  http://www.cs.utexas.edu/users/moore/acl2

SPIN http://spinroot.com/spin/whatispin.html

NuSMV http://nusmv.irst.itc.it/

Alloy http://alloy.mit.edu/

UPPAAL http://www.uppaal.com/

TLA+ and associated tools http://www.msr-inria.inria.fr/Projects/tools-for-formal-specs/

Isabelle http://isabelle.in.tum.de/  

Coq   http://pauillac.inria.fr/coq

Larch  http://www.sds.lcs.mit.edu/spd/larch/

FC2Tools http://www-sop.inria.fr/meije/verification