Theorem Raises $6M from Khosla for AI-Powered Code Verification
Theorem, a startup using AI to mathematically prove that code works correctly, has raised $6 million in seed funding, as reported by VentureBeat. Khosla Ventures led the round, with participation from Pioneer Fund, Y Combinator, e14, SAIF, and Halcyon.
The company emerged from Y Combinator's Spring 2025 batch with a simple premise: as AI generates more code, the bottleneck shifts from writing software to trusting it.
Theorem applies formal verification, a technique that uses mathematical proofs to guarantee software behaves as intended. The method has existed for decades but remained impractical for most use cases due to extreme labor costs. Co-founder Jason Gross knows this well: his PhD work at MIT on verified HTTPS cryptography took an estimated fifteen person-years.
The startup trains AI models to generate these proofs automatically, collapsing what once took years into days. In one engagement, a customer handed Theorem a 1,500-page specification and a buggy legacy codebase. Theorem produced 16,000 lines of verified production code that the customer shipped without manual review.
Gross told VentureBeat that the implications for critical infrastructure are significant:
"Now that formal verification is cheap enough, it might be considered gross negligence to not use it for guarantees about critical systems."
The team has also used the approach to surface bugs that slipped past testing at Anthropic. Current customers include AI research labs, chip designers, and GPU computing companies.
Co-founder Rajashree Agrawal described the long-term goal: "We're working on formal program reasoning so that everyone can oversee not just the work of an average software-engineer-level AI, but really harness the capabilities of a Linus Torvalds-level AI."
Theorem plans to use the funding to grow its four-person team, expand compute for training, and move into new verticals including robotics, energy, crypto, and biotech.