Verifiable AI startup Axiom raises $200M to prove AI-generated code is safe to use – News

Axiom Quant Inc. said today it’s ready to step up to the plate and make sure that the tsunami of artificial intelligence-generated code is safe, secure and accurate after raising $200 million in early-stage funding.

The Series A round, which brings Axiom’s valuation to $1.6 billion, was led by Menlo Ventures and represents a bet on a new paradigm it calls “verified AI” that aims to eliminate the risk of “hallucinations” once and for all.

Axiom’s founders are trying to tackle a fundamental flaw in the way AI creates software. Though existing tools like Claude Code and CodeRabbit can generate some truly impressive code that usually works well, their probabilistic nature is a major cause for concern.

Such tools are designed to produce outputs that look correct, as opposed to those that are provably correct. And this is a big problem, according to Menlo Ventures Partners Matt Kraning and C.C. Gong. In a blog post announcing today’s round, they said having code that “frequently works” is a “terrifying standard” when it’s going to be used in critical infrastructure systems.

“LLMs are statistical by nature — they produce plausible outputs, not provably correct or safe ones,” the partners wrote. “They can’t guarantee a function returns the right answer, and they can’t guarantee it doesn’t introduce a security vulnerability in the process. This isn’t a bug that will be fixed with the next model generation. It’s architectural. Hallucinations and unsafe code from AI are not going away.”

Axiom gets around this by training AI systems to generate formally verified outputs in Lean, which is a specialized programming language designed for mathematical proofs. By using Lean, Axiom can ensure that each step of an AI model’s reasoning process is “machine-checkable” and logically guaranteed.

It uses deterministic proof verifiers to understand whenever an output is wrong. What this means is it can provide mathematical certainty that any code function generated by an AI model will always return the correct answer. In addition, it can verify that new code snippets won’t introduce hidden vulnerabilities.

The startup first came to attention in October when it raised $64 million in seed funding, and it has made significant progress since then. In December, its deterministic AI achieved a perfect score on the Putnam Competition, which is regarded by mathematicians as the world’s most taxing undergraduate math exam. In the last century, only five humans have achieved the same perfect score, Kraning and Gong noted.

In another achievement, Axiom verifiably proved a 20-year-old number theory conjecture involving elements of calculus used to measure distances along curved surfaces. It was a challenge that Axiom’s founding mathematician Ken Ono (pictured, left) had never been able to solve, despite repeated attempts to do so over the years.

For each AI output, Axiom generates a “verified data flywheel” consisting of vast amounts of proof-checked data. This is then fed back into training loops to enhance its models’ capabilities, without introducing the risk of “model collapse,” which refers to the data pollution that causes problems with unverified AI models. In this way, Axiom operates as a recursive self-improvement loop.

The startup was founded by 25-year-old Stanford University Ph.D. student and math wizard Carina Hong (pictured, right), who graduated from MIT and serves as its chief executive. Despite her young age, she’s already a Morgan Prize winner, a Schafer Prize winner and the author of nine peer-reviewed publications. She has assembled an impressive team, including Ono, a Guggenheim, Packard and Sloan Fellow who previously served as vice president of the American Mathematical Society and is one of the world’s senior authorities on Ramanujan’s mathematics.

Axiom’s chief technology officer is former Facebook AI Research Director Shubho Sengupta, who helped to write the foundational graphics processing units libraries at Nvidia Corp. The team also includes François Charton, who was famously the first person to apply transformer models to solve a math problem that had stumped experts for more than 130 years.

The startup sees a massive opportunity to provably verify every single line of AI-generated code in a world where virtually all software is created with the assistance of large language models. “Every enterprise shipping AI-generated code is accepting unknown risk today – not just that the code might produce wrong outputs, but that it might create attack surfaces no one anticipated,” Kraning and Gong said. “Axiom eliminates both categories of risk simultaneously.”

The next step for Axiom is to scale up its training infrastructure and expand its team of math experts, with an aim to make formal verification fast and affordable for every company using AI.

Photo: Axiom Quant