In its October 2 ASIC puzzle results, Jane Street describes nearly 400 submissions from more than 30 countries. Entrants began with a physical chip layout and recovered a checker for an 11-by-11 Star Battle puzzle. Each row, column and region needed two stars, with none touching, even diagonally.
One solver’s Python model reproduced the supplied waveform while misreading every tie-high cell; an independent Verilog simulation on other inputs caught the error. Matching the fixture had hidden an incorrect adjacency check. Alejandro Soto Franco’s technical writeup goes further: it calibrates extraction against a published warm-up netlist, requires two simulators to agree, and exhausts accepted inputs rather than stopping at one solution. It is a satisfying audit trail to read over lunch. The practical question for any generated implementation is where its independent oracle comes from. Asking the same model to manufacture both the code and its confirming examples can leave a beautifully consistent mistake.