Alloy is a powerful formal specification language, but it’s historically been weak at modeling concurrency. AWS raised this as a critical issue for why they went with TLA+. Alloy writers built a lot of tricks to emulate time, but it can feel like you’re working against the language. Alloy 6 aims to change that with built-in temporal operators. Right now it’s poorly documented, and since I maintain the alloydocs, I sat down and figured it all out.
