> 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 primitiv

> 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. This is incorrect: TLA+ is also based off first-order logic constructs and can generally represent a much wider range of systems than Alloy can. The difference is that Alloy is more tractable: what it can represent it can model check much, much faster than TLA+.