It's worth pointing out that Jackson wasn't specifically thinking of TLA+ when he wrote that. In _Software Abstractions_ he compares Alloy to B, OCL, VDM, and Z. TLA+ is very different from all of those, just as Alloy is. At some point in the future I'm supposed to write an in-depth comparison, though documentation work is higher priority right now.