Z3 (and other constraint solvers) are very impressive. The most interesting application I've seen is in binary exploitation and reverse-engineering through symb

Z3 (and other constraint solvers) are very impressive. The most interesting application I've seen is in binary exploitation and reverse-engineering through symbolic execution. Angr is a very popular framework which allows for symbolic execution of binaries using Z3 as a backend. It's made a whole class of common CTF challenges almost trivial: https://docs.angr.io/docs/examples.html https://docs.angr.io/docs/examples.html