Axiom Math, a Palo Alto startup building tools to mathematically prove that AI-generated code works correctly, raised $200 million in a Series A round led by Menlo Ventures in March 2026. The company disclosed a post-money valuation of more than $1.6 billion, a remarkable jump from the roughly $300 million valuation it carried just five months earlier during a $64 million seed round.
The funding came from Menlo alongside Greycroft, Madrona, B Capital, Toyota Ventures and Triatomic Capital. B Capital, which led the October 2025 seed investment, participated again in the Series A. Menlo partner Matt Kraning joined Axiom's board as part of the deal.
At the center of Axiom's pitch is formal verification, a decades-old mathematical technique that has mostly lived in niche corners of aerospace and chip design. The startup uses the Lean theorem-proving language to generate machine-checkable proofs that software performs exactly as specified. Its AxiomProver system and AXLE API (Axiom Lean Engine) let developers turn code into mathematical certainty rather than relying on testing alone. AXLE, released March 5, became available as a cloud service for proof checking and manipulation.
"Right now, the biggest problem with using AI to write code is that you don't know when the code contains a bug," Kraning wrote when announcing the investment. Menlo framed the round around a thesis that formal verification will evolve from a specialty practice into a standard correctness layer as AI systems churn out increasing volumes of code. The firm argued the addressable market extends well beyond historical buyers of verification tools.
Founder Carina Hong left Stanford's joint JD/PhD program to start Axiom. She had been enrolled as a Knight-Hennessy Scholar. Hong graduated from MIT in 2022 with degrees in math and physics, then won the 2023 Morgan Prize, an award jointly given by the American Mathematical Society, Mathematical Association of America and Society for Industrial and Applied Mathematics. She also holds a Rhodes Scholarship. Her technical pedigree runs deep: CTO Shubho Sengupta led infrastructure work at Meta's FAIR research lab and previously worked at NVIDIA. Founding mathematician Ken Ono came aboard, as did research lead François Charton, who joined from Meta in September 2025 after working on applying transformers to mathematical problems.
The company has stacked up some eye-catching technical milestones. Axiom said its system scored a perfect 12 out of 12 on the December 2025 Putnam Competition, the notoriously difficult university-level math contest. It announced the result in February and March. Wired reported on February 4 that Axiom had solved four previously unsolved mathematical problems using its prover. By May, Axios reported that five leading journals had accepted proofs generated by Axiom's system.
"We are focused on producing journal mathematics in which human-readable proofs are paired with machine-checkable Lean formalizations," Ono told Axios in a May 26 interview.
Whether those academic accomplishments translate into enterprise traction remains somewhat unclear. Fortune reported on June 1 that Axiom had customers in finance, cybersecurity, and software and hardware development, citing the company, though no specific customers were named. Toyota Ventures' participation in the Series A signals at least one area of strategic interest: automotive software, where verification requirements are stringent and getting more so.
Menlo Ventures said Axiom would use the capital to scale research and training on verified proofs and software, productize verification tools for AI-generated code, and expand hiring. Menlo's announcement in March cited over 30 employees. By September, LinkedIn showed 54 people listing Axiom as their employer, suggesting rapid headcount growth through the spring and summer.
Competition in Lean-based verification has heated up quickly. Harmonic raised $120 million in January at a $1.45 billion valuation with backing from Nvidia's venture arm, according to Axios. Logical Intelligence released a Lean-based prover called Aleph, also in January. The field has gone from academic curiosity to venture-fundable category in the span of months, which may say as much about investor enthusiasm for anything touching AI infrastructure as it does about near-term demand for formal verification.
Still, if Menlo's thesis holds and AI-generated code becomes pervasive enough to require mathematical guarantees of correctness, Axiom finds itself well-positioned. The combination of Hong's mathematical credentials, the team's research output, and $264 million in total funding provides a substantial runway. The real test will be whether enterprises actually pay for verification tools at the scale required to justify a $1.6 billion valuation, or whether formal methods remain a specialized discipline despite the AI boom.
