I asked Claude to "fuzz the circuit" and, while it didn't work, it basically ended up going the Z3/SMT route and solving it in ~3 hours. This is after the writeups were already out, but still, as a software reverser, pretty wild. Writeup: https://www.babush.me/how-not-to-solve-jane-streets-asic-puz...