The constraint being removed here is not RTL authorship. It is RTL authorship as the rate-limiting step between a software-described specification and a physical chip. Jason Hickey published a 17-page accounting of the Salt method: one researcher, five weeks, consumer AI subscriptions, AI agents directed from application code through a verified Lean 4 compiler and executive to a RISC-V processor taped out on a community silicon shuttle. No proof passed human review. No RTL was human-written. The error ledger ran to catch #256 against zero incorrect proofs reaching the record.
The mechanism is a proof kernel that functions as the incorruptible handoff point between agents. Mathematical claims travel as kernel-checked artifacts, not prose. Human attention is reserved for statements, designs, and rulings. SAT-checked equivalence closes the gap at the silicon boundary. The agents do the mechanical work; the kernel is what makes scale possible without compounding hallucination errors. The result is a verified compiler-to-silicon chain where the human is the architect, not the implementor.
The consensus read on this kind of result is "interesting research, not ready for production." That read is probably wrong on the timeline people expect. The Salt method did not produce a production chip. It produced evidence that the bottleneck in silicon realization can be relocated from RTL authorship to specification clarity, because a Lean 4 kernel can check what an army of agents cannot. Every silicon team that treats HDL fluency as a hiring prerequisite is pricing in a bottleneck that has a 24-month expiration date.