Dec 20, 2020
• Philip Zucker
It’s that time of year again where I’m fiddling around with Z3Py. I’m booting it back up because I’m scheduled to do a tutorial on Z3 on Feb 3. It’s kind of silly because I probably already have too much content, and the tutorial is aimed at newbies, but there are some fun new things that I’ve learned in the last year I can do in Z3. As one example, it’s not so hard to build a pretty reasonable simulacrum of TLA+ in Z3.
TLA+ is a modelling/specification language for computational processes. It is particularly useful for modeling concurrency, where our intuitions fail us http://deadlockempire.github.io/. It’s the mind child of Leslie Lamport, the same guy behind LaTex and Paxos. The language doesn’t aim for deep verification of your actual code as is sometimes the goal with tools like Coq, but because of that it is significantly more lightweight and easy to use.