First time I see Z3 in the wild. Bonus points for the CLI friendly model checker, but lisp syntax... is less legible than TLA+ imho. Gotta give it a try someday to see for myself if the experience of creating the spec is better.
I've developed theorem provers with more natural syntax, and in retrospect simpler grammars are better. The stone cold truth is that most people aren't interested in using theorem provers directly; instead, they're programmatically generating queries. Simpler grammar = easier to generate, and that out-weighs direct usability.
In my next system I'll be supporting both types of grammars in the parser.
- Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan...
- Coral: https://www.microsoft.com/en-us/research/project/q-program-v...