[thomaslee]

Somewhat relevant: Pamela Zave has done some interesting work with Alloy to analyze the Chord overlay protocol:

http://www2.research.att.com/~pamela/chord.html

I'm not particularly familiar with Alloy itself, but I've found Zave's papers great for filling in the gaps in the original Chord papers.

In particular, there are multiple versions of Chord from different papers: in "How to Make Chord Correct" Zave kind of cobbles together the useful parts of the 2-3 versions of Chord from the original papers with some of her own work to produce a version of Chord that can be modeled in & verified by Spin, another lightweight verification tool:

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

[toolslive]

as a coincidence, I've been reading Pamela Zave's paper on chord myself recently. The combination of alloy's "small world hypothesis" and its ability to generate small counter examples is very useful in the context of distributed systems. Maybe it's just me, but it 'feels' a lot lighter than Coq.