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

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 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 http://spinroot.com/spin/whatispin.html