Alloy: a language and tool for relational models (2012)

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