Re Alloy
Most people that use these tools told me TLA+ and Alloy do different things with their automated tooling. They usually say TLA+ looks at ordering of things with Alloy looking at structuring. I only found a few people comparing them directly, though. Do you have a resource showing TLA+ does same thing as Alloy or as easily?
Re SPIN
Im saying they were used similarly. You wrote in one artocle like set theory, model-checking for temporal errors, and so on are new. That was the default in high-assurance decades ago using things like Z specs with SPIN for concurrency. Then, they tried to go for verifying high-level code, then rough code, code then assembly, and so on with refinement proofs. However, it started with algorithmic verification with specs in set theory, first-order logic, and ASM's. Writeups like yours tell me Lamport's concept was to similarly use those easier formalisms leaving off anything but the algorithm. Then add more automation to get more bang for buck for more developers. A good idea since the subset of that which Z and SPIN offered had already prevented serious, sometimes deep, errors in prior systems.
Now, far as SPIN, it was used to chech the properties of concurrency models, hardware specs, caching, protocols, standards, and distributed systems. Industry found bugs in all these things using it with relatively little training vs other methods that required rare specialists. Sound familiar? TLA+ now shows up as tool of choice for quite a few of those areas with SPIN still used a lot due to maturity & being well-known. That's why I said they're similar: people are specifying and model checking similar things with them similarly with much less effort than provers.
The easier proving on TLA+ and high-level nature are real benefits ovee SPIN. It's why I recommend TLA+. ;)