I've experimented quite a lot with Coq, and am still struggling to get value from it in a distributed systems context. TLA+ (<a href="http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html" rel="nofollow">http://research.microsoft.com/en-us/um/people/lamport/tla/tl...</a>), on the other hand, was useful to me from the first day that I tried to use it. It's model seems better suited to demonstrating properties of distributed systems, and often the exhaustive testing approach of TLC provides much of the same value that Coq's proofs do.<p>Coq and TLA+ obviously solve different problems, so comparing them directly isn't possible. For a first step into formal methods for distributed systems engineers, however, I'd recommend TLA+ based on my experiences.