Axiom Math raises $200M to verify AI-generated code with mathematics

What's the deal? Palo Alto-based Axiom Math has raised $200M from Menlo Ventures, Greycroft, and Madrona, valuing the year-old, 20-person startup at $1.6B. Its bet: use formal mathematics to automatically verify that AI-generated code is safe and correct.

The funding comes as AI coding tools go mainstream — and as their tendency to produce buggy code becomes a growing liability.

Why now? A Carnegie MellonDealroom has a profile for this one. Try Dealroom → study published in January 2026 found that while AI coding tools speed up development, they can degrade code quality over time. The gap created an opening for Carina HongDealroom has a profile for this one. Try Dealroom →, Axiom's chief executive officer and founder, who has built her company around the idea that mathematics can be the arbiter of code correctness.

Axiom's core technology, AxiomProver, uses Lean — a programming language originally designed to prove mathematical statements — to verify whether code does what it is supposed to do.

AxiomProver's credentials are hard to dismiss. In December 2025, it achieved a perfect score on the Putnam Exam, an annual competition widely regarded as the most prestigious maths contest for undergraduate students in North America. Researchers call the move from proving maths to verifying code "transfer learning," and early benchmark results suggest the technique holds up.

What could go wrong? Maths has clear right and wrong answers; software does not. "You can't always specify what it means for computer code to be correct," said Bogdan VasilescuDealroom has a profile for this one. Try Dealroom →, a Carnegie Mellon computer science professor. Real-world applications — social media platforms, for instance — must handle complexity that no formal proof can fully anticipate.

The signal: Axiom is not alone. Rival Harmonic, also in Palo Alto, is valued at $1.45B after its own funding round in 2025, and Logical IntelligenceDealroom has a profile for this one. Try Dealroom → in San Francisco is pursuing a similar approach.

Investors are making a clear bet: as AI writes more of the world's code, the ability to verify it mathematically becomes critical infrastructure. The question is how far formal verification can reach before it hits the limits of what maths can prove.

Sources:
Menlo Ventures
SiliconANGLE
National Today
The New York Times
The New Zealand Herald
Axiom Math's LinkedIn post

Image credit:
Axiom Math

J.V.