Microsoft's Z3 Guide Lets You Try the Prover in Your Browser
Online Z3 Guide
Microsoft Research has published an online guide to Z3, the widely used SMT solver. The site offers an SMTLIB tutorial, a Programming Z3 section with JavaScript examples, and a playground for freeform editing. It also links to the Python guide, GitHub repository, API docs, and slides. The guide is built with Docusaurus and lists z3-solver 5.0.0 on npm.
Online Z3 Guide
- olooney
I like Z3 a lot. I think it's criminally underappreciated and underused. Here is a fairly interesting use I put it to a few years ago:
https://www.oranlooney.com/post/playfair/#known-plaintext-at...
Slightly more complicated than the toy examples shown in the documentation above, and hints at one of the real world use cases for Z3 - red teaming cryptography.
That said, I'm not sure the documentation linked above is really doing it any favors in terms of helping popularizing it.
- greatgib
If anyone wondering, because it took me a few hops to find out:
Z3 is a high-performance theorem prover being developed at Microsoft Research.