Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.


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-lan...

- Coral: https://www.microsoft.com/en-us/research/project/q-program-v...

- Ivy: https://github.com/microsoft/ivy


You nailed it, that's exactly what we use Z3 for in Apalache, a symbolic model checker for TLA+: https://apalache.informal.systems


Ahh, neat. Indeed, checking SAT felt a bit more generally applicable than checking SAT for temporal behaviors.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: