AI Will Write All the Code. Mathematics Will Prove It Works.

We are approaching a world where AI writes effectively all software. Agentic coding tools are already producing entire applications, and the capabilities are improving monthly. But there’s a problem hiding inside this revolution that almost no one is talking about: None of the code is verified.

Large language models generate code that looks right. It compiles, it often passes tests, and it frequently works. But “frequently works” is a terrifying standard for the systems that run our infrastructure, manage our finances, and protect our data. LLMs are statistical by nature—they produce plausible outputs, not provably correct or safe ones. 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 is the company that solves this.

Today, I’m announcing that Menlo Ventures is leading Axiom’s Series A of $200 million at a $1.6 billion post-money valuation, and I’m joining the board.

Proofs, Not Predictions

Axiom’s approach is architecturally distinct from everything else in AI. Rather than generating statistically likely outputs, Axiom trains systems to produce formally verified outputs in the programming language Lean. Every output is machine-checkable and verifiable. Every reasoning step is logically guaranteed to be correct. When the system produces a flawed proof, the error is caught deterministically—the system literally knows when it’s wrong.

This is Verified AI. It cannot hallucinate, and it can prove its outputs are safe.

The implications for code are immediate and twofold. Formal verification doesn’t just prove that code produces the right output—it also proves that code doesn’t do things it shouldn’t. A verified function can be guaranteed to always return the right answer for every input, to never corrupt data during a transaction, to never overflow a buffer, and to never introduce the kinds of subtle security vulnerabilities that human reviewers and test suites routinely miss. This is correctness and safety, proven mathematically, before code ever runs in production.

This transforms AI code generation from a probabilistic gamble into something enterprises can actually trust. Not “it passed our tests” trust, but mathematical certainty.

Sixth Perfect Score in 98 Years

Axiom started operating in July 2025. In under seven months, the company achieved results that dwarf competitors with years more runway and hundreds of millions more in funding.

The headline: In December 2025, Axiom scored a perfect 12/12 on the Putnam Competition, the hardest undergraduate math exam in the world. Out of more than 150,000 attempts, only five humans have ever achieved perfection in 98 years. The median human score is zero. No other company achieved perfection in 2025.

But the Putnam is only the beginning of what we’ve seen. The same AI—unmodified—automatically proved a 20-year-old open number theory conjecture that even Ken Ono, one of the world’s top number theorists and Axiom’s Founding Mathematician, could not solve himself. We have also seen early but striking signs of transfer learning into software verification domains, despite this model having no training on any concepts of software engineering, computers, or even code—only logic.

Underpinning all of this is a verified data flywheel that no other AI system can replicate. Axiom has generated many orders of magnitude more formally verified data than all previously available human-produced sources combined. Because this data is checked by deterministic proof verifiers, it feeds cleanly back into training—unlike unverified data domains, where AI-generated data must be filtered out of training data to prevent data pollution and model collapse. The result is a recursive self-improvement loop gated only by compute, and structurally impossible for standard LLMs to replicate.

Together, these breakthroughs suggest Axiom may be approaching a GPT-3-like inflection in Verified AI—one where scaling is limited only by compute, not by human-generated data.

The TAM Is All AI Code

I want to be precise about the market opportunity. We are not underwriting Axiom to the traditional formal verification market, which has historically been low single-digit billions of dollars and limited to mission-critical systems at organizations like NASA and AWS. That market was small because it required Ph.D.-level expertise and 20 lines of proof for every line of code.

Axiom increasingly automates this process from the bottom up, starting with individual functions and modules. When formal verification becomes fast, cheap, and automatic, the addressable market is the right of first refusal to generate every line of AI-generated code that has any consequence.

The safety dimension alone is enormous. 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. Axiom eliminates both categories of risk simultaneously.

AI code generation will soon encompass virtually all software development. Axiom is building the correctness and safety layer for that future. It’s one of the most differentiated positions in the AI coding ecosystem we’ve encountered.

Carina Hong and a Generational Team

The founder matters as much as the technology. Founder CEO Carina Hong is a 25-year-old Rhodes Scholar and MIT graduate who left a Stanford J.D./Ph.D. in Mathematics (Knight-Hennessy) in her first year to build Axiom. She is a Morgan Prize winner, Schafer Prize winner, and author of nine peer-reviewed publications. I’ve worked closely with her since Axiom began operating, and her combination of mathematical depth, ability to attract and retain truly world-class talent, and sheer operational velocity is as impressive as any founder I’ve encountered in two decades in Silicon Valley.

The team she’s assembled in seven months is extraordinary and contains numerous “N of 1” unique talents. Shubho Sengupta, Axiom’s CTO, a former Facebook AI Research Director, spent eight years leading billion-dollar-plus research infrastructure efforts at Meta and wrote foundational GPU libraries at NVIDIA. François Charton, who, in 2019 was the first person to apply transformers to mathematics—pioneering the entire AI-for-math field that Axiom now leads—joined after using LLMs at Meta AI to solve a 130-year-old math problem and disprove a 30-year-old conjecture. Ken Ono—a Guggenheim, Packard, and Sloan Fellow, recipient of a Presidential Early Career Award from Bill Clinton, former Vice President of the American Mathematical Society, and one of the world’s foremost authorities on Ramanujan’s mathematics—resigned a tenured professorship and his role as Vice Provost at UVA to join Axiom full-time. Over a career spanning four decades and dozens of top Ph.D. students, he has mentored 10 Morgan Prize winners—including Carina herself. The company has grown to over 30 employees with unusually deep expertise spanning AI, mathematics, and code generation—and the recruiting pipeline continues to accelerate.

The Bet

This round funds additional world-class technical hiring and the ability to scale training on Axiom’s expanding corpus of verified proofs and verified software—the moment where we expect another step-change in capability—and bring initial products to market.

We’re betting that Verified AI is a new paradigm, not an incremental improvement. That proving code is both correct and safe will become as essential as generating it. That code verification is the first market, not the last. And that Carina, Shubho, Ken, François, and the entire Axiom team are building the defining Verified AI company for the entire world.

Menlo Ventures is proud to lead this round.