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. --- --- REFERENCES: person: [00:00:10] Thomas Ahle https://thomasahle.com organization: [00:00:27] Normal Computing https://normalcomputing.com/ paper: [00:00:27] Subsets and Supermajorities: Optimal Hashing-based Set Similarity Search https://arxiv.org/abs/1904.04045 [00:00:27] Clustering the Sketch: Dynamic Compression for Embedding Tables https://arxiv.org/abs/2210.05974 [00:11:21] ProgramBench: Can Language Models Rebuild Programs From Scratch? https://arxiv.org/abs/2605.03546 [00:23:50] Autoformalization with Large Language Models https://arxiv.org/abs/2205.12615 [00:31:55] Autoformalizing Memory Device Specifications with Agents https://arxiv.org/abs/2605.00058 [00:35:20] Thermodynamic AI and the Fluctuation Frontier https://arxiv.org/abs/2302.06584 [00:36:40] Thermodynamic Computing 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 [00:49:45] Chain of Thoughtlessness? An Analysis of CoT in Planning https://arxiv.org/abs/2405.04776 tool: [00:33:05] TLA+ https://lamport.azurewebsites.net/tla/tla.html [00:44:50] Stockfish https://en.wikipedia.org/wiki/Stockfish_(chess) 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:02:55] World's first thermo chip reaches tape out https://www.tomshardware.com/tech-industry/semiconductors/worlds-first-thermodynamic-computing-chip-reaches-tape-out-normal-computings-physics-based-asic-changes-lanes-to-train-more-ai [00:30:00] Math Does Not Represent https://www.youtube.com/watch?v=aA_T20HAzyY [00:32:02] DRAMBench: Autoformalizing DRAM Specifications with Timed Petri Nets https://www.iese.fraunhofer.de/blog/drambench-autoformalizing-dram-specifications/ [00:35:20] Extropic, Normal Computing, and D-Wave? https://www.zach.be/p/whats-the-difference-between-extropic --- ReScript: https://app.rescript.info/share/ff9684a112ab37744096adaeb097a263