SPIN
SPIN is an efficient LTL model checker for distributed software designs, and is possibly the most widely used concurrency verification tool. The tool supports a high level language to specify systems descriptions, called PROMELA (a PROcess MEta LAnguage). Spin has been used to trace logical design errors in distributed systems design, such as operating systems, data communications protocols, switching systems, concurrent algorithms, railway signaling protocols, etc. The tool checks the logical consistency of a specification. It can be used as a simulator, as an exhaustive verifier, or as proof approximation system. Spin works on-the-fly, provides direct support for the use of embedded C code, and works on-the-fly.
http://spinroot.com

The Stanford Temporal Prover
The Stanford Temporal Prover, STeP, is being developed to support the computer-aided formal verification of reactive, real-time and hybrid systems based on their temporal specification. Unlike most systems for temporal verification, STeP is not restricted to finite-state systems, but combines model checking with deductive methods to allow the verification of a broad class of systems, including parameterized (N-component) circuit designs, parameterized (N-process) programs, and programs with infinite data domains.
http://www-step.stanford.edu

Murphi
Murphi is a verifier based on explicit state enumeration. The verifier performs depth- or breadth-first search in the state graph defined by a Murphi description language. Murphi can be used for several different verification tasks. Applications include Verification of the cache coherence protocols in Stanford's DASH and FLASH multiprocessors.
http://verify.stanford.edu/dill/murphi.html

CADP
Construction and Analysis of Distributed Processes", formerly known as "CAESAR/ALDEBARAN Development Package", is a popular toolbox for the design of communication protocols and distributed systems.
http://www.inrialpes.fr/vasy/cadp.html