This is such weird timing, for the last few weeks I’ve been messing around with Z3 and other solvers for the first time and they’re so cool. In many ways more magical than LLMs to me in some ways. Great intro!