Oh hey, I worked on this a while back. At the end of 2021 I also did work for Teleport extending this same approach and applying it to Role-Based Access Control

Oh hey, I worked on this a while back. At the end of 2021 I also did work for Teleport extending this same approach and applying it to Role-Based Access Control rules. This was interesting because it exercised Z3's string analysis capabilities, even checking regular expressions for equivalence: https://ahelwer.ca/post/2022-01-19-z3-rbac/ https://ahelwer.ca/post/2022-01-19-z3-rbac/ People get intimidated by the terms SMT or theorem prover but I want to emphasize this is actually a really simple process. Any time you have two sets of logical rules (often found in access control systems) you want to compare, translating them into Z3 is really quite easy. There are Z3 bindings in lots of languages, I used Python for the Teleport work: https://github.com/gravitational/rbac-linter https://github.com/gravitational/rbac-linter My friends and I have also used Z3 to solve various math puzzles. It's useful for checking whether a solution exists when you start modifying the puzzle to see how far you can push it. We used it for this puzzle, for example: https://www.nsa.gov/Press-Room/News-Highlights/Article/Article/1627320/august-puzzle-periodical-50-for-all/ https://www.nsa.gov/Press-Room/News-Highlights/Article/Artic...