"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.
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).
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.
I once left a comment on a submission that seemed to go through the second chance pool twice before getting traction, picking up three sets of replies each 24 hours apart.
