Allow is very different in that it approaches things by converting whatever you are trying to verify into first order logical formulae then trying to find some

Allow is very different in that it approaches things by converting whatever you are trying to verify into first order logical formulae then trying to find some model which violates the formula. This is undecidable in the general case, but Alloy works around this by limiting the domain to some finite size (so considering all possible sets below some size) in which case the problem is merely NP-complete and easily translated into SAT. Because Alloy works off of first order logic, it's a lot more general than TLA+ but doesn't have temporal logic concepts like liveness as first class primitives. You can still model most of this stuff in Alloy, but I think Alloy is really best for when you want to verify something which doesn't have a good model checker available or in problem spaces which easily reduce to first order logic.