Z3 is intended as more of a backend for higher-level languages, like TLA+, to use in model checking. I would be surprised if anyone were writing specs in the input language directly.
- Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan...
- Coral: https://www.microsoft.com/en-us/research/project/q-program-v...