It's more geared towards the static elements of the system, and writing a spec feels quite like writing a relational database schema -- mostly because they're both expressions of relationships.
It seems like a pretty natural path to write a spec in alloy before building out some crud interface.
I think there's a huge tooling gap though. Alloy, TLA+ and friends all seem to be very jvm/UI centric, really targeting a user who is working in the editors the language ships with.
I'd really love to see more tooling to run model checkers in a CI pipeline, or generate stubs and test cases for various languages. If that were in place, I think there would be more stickiness to formal methods.
I've started writing a Go parser for alloy, in part to learn it better, in part because I know go and want to write some tooling that I think go would be a good implementation language for. I don't know if anything will come of it, but at least having a parser would allow for things like a formatter or code generator. If I were feeling ambitious, I might try to implement a model checker.