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
Java
Modeling Language (JML)
Extended
Static Checker for Java
Bandera
Labelled
Transition Analyzer (LTSA)
Daikon
invariant detector
FDR2
ACL2 http://www.cs.utexas.edu/users/moore/acl2
SPIN http://spinroot.com/spin/whatispin.html
NuSMV
Alloy
UPPAAL
TLA+ and associated tools http://www.msr-inria.inria.fr/Projects/tools-for-formal-specs/
Isabelle
Coq http://pauillac.inria.fr/coq