Z3 is a powerful framework developed by Microsoft Research. Given a list of restrictions and conditions, Z3 finds one solution that satisfies them all, if that solution exists. It can be used for multiple purposes but some known uses in security are exploiting or checking firewall rules. It is also a handy tool for solving many CTF challenges related to encryption and keygen generation.

https://infosecadalid.com/2021/08/27/my-introduction-to-z3-and-solving-satisfiability-problems/