Theorem wants to stop AI-written bugs before they ship — and just raised $6M to do it
Theorem wants to stop AI-written bugs before they ship — and just raised $6M to do it
Publish Date: 2026-01-27 09:00:00
Source Domain: venturebeat.com
As artificial intelligence reshapes software development, a small startup is betting that the industry’s next big bottleneck won’t be writing code — it will be trusting it.
Theorem, a San Francisco-based company that emerged from Y Combinator’s Spring 2025 batch, announced Tuesday it has raised $6 million in seed funding to build automated tools that verify the correctness of AI-generated software. Khosla Ventures led the round, with participation from Y Combinator, e14, SAIF, Halcyon, and angel investors including Blake Borgesson, co-founder of Recursion Pharmaceuticals, and Arthur Breitman, co-founder of blockchain platform Tezos.
The investment arrives at a pivotal moment. AI coding assistants from companies like GitHub, Amazon, and Google now generate billions of lines of code annually. Enterprise adoption is accelerating. But the ability to verify that AI-written software actually works as intended has not kept pace — creating what Theorem’s founders describe as a widening “oversight gap” that threatens critical infrastructure from financial systems to power grids.
“We’re already there,” said Jason Gross, Theorem’s co-founder, when we asked whether AI-generated code is outpacing human review capacity. “If you asked me to review 60,000 lines of code, I wouldn’t know how to do it.”
Why AI is writing code faster than humans can verify it
Theorem’s core technology combines formal verification — a mathematical technique that proves software behaves exactly as specified — with AI models trained to generate and check proofs automatically. The approach transforms a process that historically required years of PhD-level engineering into something the company claims can be completed in weeks or even days.
Formal verification has existed for decades but remained confined to the most mission-critical applications: avionics systems, nuclear reactor controls, and cryptographic protocols. The technique’s prohibitive cost — often requiring eight lines of mathematical…
