tl;dr: The author tackled Jane Street's ASIC reverse engineering challenge, which involves extracting a circuit from a GDS file and finding a 120-bit input that produces a specific output. After building unnecessary custom tooling (simulator, HDL parser, GDS viewer), they eventually used the gdstk Python library to extract components, converted the circuit to Verilog, and used the Z3 constraint solver to work backwards from the desired output to find the correct input. Along the way, they discovered a legitimate bug in Jane Street's circuit design.