Theorem Labs

Theorem Labs (operating as Theorem) is an AI and programming languages research lab founded in 2025 by Jason Gross and Rajashree Agrawal and headquartered in San Francisco, California. The company emerged from Y Combinator's Spring 2025 batch with a focus on a central question: as AI models become better at generating code, what is the bottleneck to safely deploying vastly more computation in the world? Formal verification — the use of mathematical proofs to show that software conforms exactly to its specification — is Theorem's core technology. Traditional formal verification is prohibitively expensive and slow, often taking teams years to verify even small codebases. Theorem's approach, which they call fractional proof decomposition, allocates verification effort proportionally to the risk or importance of each code component rather than exhaustively testing every possible behavior. Their AI models are trained to make program verification orders of magnitude faster. The team developed SFBench, a benchmark that demonstrated AI translation of 1,276 formal proof problems from the Logical Foundations textbook, achieving a 350x speed-up over manual methods. In a notable real-world application, their tools identified a bug in Anthropic's top-k sampling code that had slipped past standard testing. In January 2026, Theorem announced a $6 million seed round led by Khosla Ventures, 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 Tezos). At the time of the announcement, the company had four employees and planned to use the capital to expand the team, increase compute resources for training verification models, and enter new verticals including robotics, renewable energy, cryptocurrency, and drug synthesis. Theorem operates as a Public Benefit Corporation (PBC). Their customers include AI labs, electronic design automation firms, and GPU-accelerated computing companies.