4 ms·

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 someda

• ahelwer 6y ago
  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.
  • romac 6y ago
    You nailed it, that's exactly what we use Z3 for in Apalache, a symbolic model checker for TLA+: https://apalache.informal.systems https://apalache.informal.systems
  • igornotarobot 6y ago
    True. There are many frontends for Z3 that focus on various domains. For instance, those developed at Microsoft: - Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan... - Coral: https://www.microsoft.com/en-us/research/project/q-program-verifier/ https://www.microsoft.com/en-us/research/project/q-program-v... - Ivy: https://github.com/microsoft/ivy https://github.com/microsoft/ivy
  • villasv 6y ago
    Ahh, neat. Indeed, checking SAT felt a bit more generally applicable than checking SAT for temporal behaviors.
• throwawaygh 6y ago
  > but lisp syntax... is less legible than TLA+ imho. 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.