SaltWorks, from application code to silicon

Over the summer I ran an experiment. Could one person, on consumer AI subscriptions, direct a small fleet of AI agents to build a verified stack all the way from application code down to a chip? The result is SaltWorks, and the paper describing it is arXiv:2608.21356, “AI with Authority, from Application to Silicon.”

In five weeks, the agents built application programs with their specifications, a compiler and an executive verified in Lean 4, and a chip that went out on the Tiny Tapeout community shuttle TTSKY26c. No proof passed through human review, and no RTL was written by a human.

The referee

For sixty years, machine verification has been an overhead that only exceptional projects could afford. My argument in the paper is that generative AI turns this around. When agents write code and proofs at machine speed, a proof kernel becomes the thing that makes the work trustworthy at all: a referee that a hallucinated proof cannot get past. Claims travel between agents as kernel-checked artifacts, and my own attention goes to statements, designs and rulings.

We call the working discipline the Salt method. Every objective returns five artifacts: an implementation, a specification, a proof that the implementation meets the specification, adversarial tests, and short certificates that make the specification easy for a person to check. No claim is admitted without its checker. Errors and retractions are kept in an append-only ledger as results in their own right; the error ledger of the mathematics campaign in the paper runs to catch #256, against zero incorrect proofs reaching the record.

The chip

The chip is a bit-serial neural dataflow fabric: signed multiply-accumulate cells on an 8-port self-routing banyan switch, with a small RISC-V processor beside them sharing the same 24 pins. Each multiply-accumulate cell is generated from a Lean model proved correct by the Lean kernel, and the generated netlist is then proved equivalent to its arithmetic specification over all inputs by a SAT solver; the signed accumulation is proved for the drive schedule the design specifies. The datasheet states exactly which parts are proved and which are not: the sequencer, the pin wrapper and the fabric glue are RTL written directly, outside either proof.

What we got wrong

The RISC-V core on the chip was not verified by the method. Lean proves a 7-instruction model of the core, but no theorem connects that model to the fabricated design, and no conformance suite was run before tapeout. The first conformance run, after submission, found 3 of 31 in-scope instructions failing: SRA, SRAI and LW. The causes and measured software workarounds are in the erratum, and the datasheet carries the same text.

I find this the most instructive part of the project. The defects were found in the one layer of the stack the kernel never checked.

The record

The record is public:

The agents were Claude models from Anthropic, working under my direction, with the Lean kernel as the final referee for every formal claim.