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 generat

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.