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