I've been learning Alloy[0], which I think is probably more practical for most software engineers. I'm using it with the goal of documenting and decomposing a

I've been learning Alloy[0], which I think is probably more practical for most software engineers. I'm using it with the goal of documenting and decomposing a legacy system that I've been working with for a number of years. 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. [0] https://alloytools.org/ https://alloytools.org/