Thomas Ahle wants Normal Computing to be the Lovable for chip design: type your intent, and a swarm of agents carries it from design through optimisation, formalisation and verification to tape-out. To get there, his team at wrote their own open-source Verilog simulator, 580,000 lines in 43 days, because commercial EDA verifiers run about $10,000 per core and there are no decent open-source compilers to build on.

That sets up the question Tim keeps pressing: if an agent can produce a chip design, a proof, or a working program, how do you actually know it is correct? Passing 70% of tests is not the same as being right, and a single fabricated bug can cost a company a fortune. They dig into ProgramBench (rebuild a program from its tests, roughly 0% success), the difference between structure and competence, and the "understanding debt" you take on when nobody reads the code.

From there: auto-formalisation in Lean and the AlphaProof trick of training on prove-or-disprove; why there is no single true representation of a spec (Petri nets, TLA+, Erik Curiel's "math does not represent"); and thermodynamic computing, where Normal Computing's CN101 chip is built so that its physical noise *is* the computation, settling a stochastic differential equation in hardware to invert a matrix. Plus Bayesian uncertainty, specialisation, the Chomsky hierarchy, AI slop, and whether performance is all that matters.

Recorded in Zurich.

Disclosure: Normal Computing paid our production and travel costs for this show. We retained full editorial control. They did not see the video before publication, and we did not show it to them or discuss it with them beforehand.

---

TIMESTAMPS:

00:00:00 Meet Thomas Ahle: the Lovable for chip design

00:03:41 Why hardware needs formal verification

00:06:36 Ten thousand dollars per core and a six-month agent run

00:07:40 Rebuilding programs from tests: ProgramBench and zero percent

00:12:15 Structure vs competence: can you learn a program from behavior?

00:15:27 Continual learning, abstraction, and Claude as an ecosystem

00:23:17 Autoformalization and the AlphaProof trick

00:29:31 No single true representation: specs, Petri nets and TLA+

00:34:43 Thermodynamic computing: when noise is the computation

00:37:32 Bayesian uncertainty in the age of token streams

00:41:12 Hybrid compute: vibe-coding loops, binaries and Stockfish

00:44:44 Co-design, central-AI apps and API pricing

00:49:45 Chain of thoughtlessness and the Chomsky hierarchy

00:53:40 AI psychosis, slop and the broken social contract

00:57:34 Typing it yourself, teamwork and performance vs competence

---

REFERENCES:

person:

[00:00:10] Thomas Ahle

https://thomasahle.com

organization:

[00:00:27] Normal Computing

https://normalcomputing.com/

paper:

[00:11:21] ProgramBench: Can Language Models Rebuild Programs From Scratch?

https://arxiv.org/abs/2605.03546

[00:31:55] Autoformalizing Memory Device Specifications with Agents

https://arxiv.org/abs/2605.00058

[00:35:20] Thermo AI and the Fluctuation Frontier

https://arxiv.org/abs/2302.06584

[00:36:40] Thermo Comp System for AI Applications

https://arxiv.org/abs/2312.04836

[00:37:05] Thermodynamic Linear Algebra

https://arxiv.org/abs/2308.05660

[00:44:50] An efficient probabilistic hardware architecture for diffusion-like models

https://arxiv.org/abs/2510.23972

tool:

other:

[00:01:00] Building an Open-Source Verilog Simulator with AI: 580K Lines in 43 Days

https://normalcomputing.com/blog/building-an-open-source-verilog-simulator-with-ai-580k-lines-in-43-days

[00:02:55] Normal Computing Announces Tape-Out of the World's First Thermodynamic Computing Chip (CN101)

https://www.normalcomputing.com/blog/normal-computing-announces-tape-out-of-worlds-first-thermodynamic-computing-chip

[00:32:02] DRAMBench: Autoformalizing DRAM Specifications with Timed Petri Nets

https://www.iese.fraunhofer.de/blog/drambench-autoformalizing-dram-specifications/

---

ReScript: https://app.rescript.info/share/ff9684a112ab37744096adaeb097a263