LLMs beat specialized tools at building circuits from scratch

Reactive synthesis — automatically generating hardware circuits from logical specifications — has resisted automation because it's computationally hard and requires writing precise temporal logic by hand. This system wraps a large reasoning model in a repair loop: it generates Verilog, then uses a model checker to produce symbolic counterexamples, and iterates until the circuit is correct. That loop outperforms specialized tools from the annual synthesis competition and even handles parameterized systems, which are formally undecidable. A separate autoformalization step, backed by a new hand-authored dataset, lets engineers specify behavior in plain English rather than temporal logic, with comparable synthesis success rates.