Show notes
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 design00:03:41 Why hardware needs formal verification00:06:36 Ten thousand dollars per core and a six-month agent run00:07:40 Rebuilding programs from tests: ProgramBench and zero percent00:12:15 Structure vs competence: can you learn a program from behavior?00:15:27 Continual learning, abstraction, and Claude as an ecosystem00:23:17 Autoformalization and the AlphaProof trick00:29:31 No single true representation: specs, Petri nets and TLA+00:34:43 Thermodynamic computing: when noise is the computation00:37:32 Bayesian uncertainty in the age of token streams00:41:12 Hybrid compute: vibe-coding loops, binaries and Stockfish00:44:44 Co-design, central-AI apps and API pricing00:49:45 Chain of thoughtlessness and the Chomsky hierarchy00:53:40 AI psychosis, slop and the broken social contract00:57:34 Typing it yourself, teamwork and performance vs competence---REFERENCES:person:[00:00:10] Thomas Ahlehttps://thomasahle.comorganization:[00:00:27] Normal Computinghttps://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 Agentshttps://arxiv.org/abs/2605.00058[00:35:20] Thermo AI and the Fluctuation Frontierhttps://arxiv.org/abs/2302.06584[00:36:40] Thermo Comp System for AI Applicationshttps://arxiv.org/abs/2312.04836[00:37:05] Thermodynamic Linear Algebrahttps://arxiv.org/abs/2308.05660[00:44:50] An efficient probabilistic hardware architecture for diffusion-like modelshttps://arxiv.org/abs/2510.23972tool:other:[00:01:00] Building an Open-Source Verilog Simulator with AI: 580K Lines in 43 Dayshttps://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 Netshttps://www.iese.fraunhofer.de/blog/drambench-autoformalizing-dram-specifications/---ReScript: https://app.rescript.info/share/ff9684a112ab37744096adaeb097a263