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

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