Creatively Misusing TLA+

Even the general constraint solver? There are tools like Z3 which are designed to solve this sort of problem (quickly and exhaustively), and then there are tools like TLA+ which can solve this sort of problem (slowly and exhaustively).

"Creative misuse" refers to intended use. TLA+ isn't "meant" for these things, it just happens to be good for some (and kinda-okay for others). But that's the beauty of tools: it doesn't matter what they were designed to do, you can use them for whatever you need them to do.

It's harder to find creative misuses for programming languages because they're "intended" be general purpose. They're more like a material than a tool.

It's a misuse in the same way using a flathead screwdriver to pry something open is a misuse. It may be a reasonable way to get the job done, but it's not what a screwdriver is designed for.

This looks like a second-chance pool story as it didn't get much attention last time it was posted.

See dang's comments on the pool here: https://news.ycombinator.com/item?id=26998308