Interchange: change here between the Hardware and ML lines.
SlackSmith
Why
Changing how many clock cycles a circuit takes should not silently change what it computes. Timing fixes usually come with a prayer. A language model writing those fixes makes that worse, because its wrong answers read exactly like its right ones. SlackSmith makes every change come with a proof, and then asks the harder question: did the change actually buy anything once the chip is laid out.
How
One command does what an engineer otherwise does by hand. It fingerprints the timing constraints so an edit to them cannot pass as a win, builds the circuit, finds the slowest path, and decides whether the fix belongs in the wiring or in the design itself. A model proposes a rewrite and declares what kind of change it is; that declaration picks the proof the rewrite has to pass. Then the circuit is timed again and the change is kept or thrown away on the measurement, not on the promise. Every decision is written down with the evidence behind it.
What came out
A loop that can be run from a clone, with five proof branches proven and four routed automatically, and a record of every decision and the evidence for it. The constraint check earns its place on its own: one line of constraints is worth 5.179 ns on a byte-identical netlist, and every equivalence checker correctly calls the two designs identical, so without that check a constraint edit would read as a timing win. The method is now being tested on its own, outside this benchmark: a follow-on project runs it head to head against a plain, non-AI timing-closure optimizer on ten more designs. Interim score: 7 of 11 pre-registered predictions correct, the model arm not built yet.
What broke
Three things, and they are the point of the project. The model proposes rewrites that are wrong: of 12 proposals frozen before any check ran, 3 were formally refuted, and one of those passed every precondition, cut 208 cells and survived the design firmware and 20,000 random instruction vectors before the proof gate produced a counterexample in 46 seconds. On the main benchmark the correct rewrites bought nothing that lasted: three proven transforms worth 5.165 ns on paper became 0.000 after buffering and slightly negative after repair, because the slow paths were dominated by wiring, not logic. And the one result that did survive came from a proposer that turned out to have tools and could read earlier results, which is disclosed rather than quietly claimed; running it blind produced nothing better than the control. One surviving gain is one result, not a rate.