Here are some interesting systems for doing formal methods (also here, and here): the modelling notations Alloy, AsmL, TLA, Unity, VDM, and Z (also here), the theorem provers ACL2, PVS, and Z/EVES, and the model-checkers SMV (also here), Spin, and Alloy again.
Also, the programming language Spec#, along with its static checker and verifier, and its modeling and testing tool Spec Explorer (also here, and here).