"Using lightweight modeling to understand Chord" (Pamela Zave; ACM SIGCOMM Computer Communication Review, 42(2):50-57, April 2012) summarizes the results of modeling and analyzing the Chord ring-maintenance protocol with Alloy. The paper proves that no published version of Chord is correct, even when obvious bugs are fixed.
More recently, I have discovered a correct version of Chord, and proved that it is correct. This work is presented in the talk "A correct version of Chord (and how to get it)" and in the paper "A practical comparison of Alloy and Spin" (Pamela Zave; submitted for publication, 2013).
"Experiences with protocol description" (Pamela Zave; 1st International Workshop on Rigorous Protocol Engineering, Vancouver, Canada, October 2011) explains the nature of some of the flaws in the prior informal reasoning about Chord.
The original paper on this work, "Lightweight verification of network protocols: The case of Chord" (Pamela Zave; AT&T Technical Report, January 2010), gives a complete explanation of how to use Alloy to prove that a subset of Chord is correct.
For those who wish to see the Alloy code, chordjoin.als is the subset of Chord in which members of the network cannot leave or fail, chordfull.als is the full Chord protocol as specified in the SIGCOMM paper (with borrowing from another paper to fill gaps), and chordbest.als is what appears to be the best version of the protocol, taking pieces from the three published papers.