For those like me who didn't know what Alloy is, it looks like it's a general purpose constraint solver for testing correctness in range of different algorithms.
It can be used to model not only algorithms but principally concepts.
I always use Alloy before starting a new design.