There’s a certain kind of founder who doesn’t pick a problem because it’s tractable. They pick it because they can’t stop thinking about it, because the gap between what exists and what should exist is too important to solve. Carina Hong is that kind of founder.
The company she and her team are building, Axiom Math, is tackling one of the most consequential problems in AI: how to verify the output of non-deterministic systems. And, specifically, how do you know when AI-generated code is provably correct, with enough rigor to stake a critical system on it? Today, Axiom announced $200 million in new funding to deliver scalable verification solutions.
Carina has been drawn to the edges of mathematical reasoning since she was a teenager, writing nine research papers across number theory, combinatorics, and probability during her undergraduate years at MIT. When a friend introduced her to Lean, a programming language that turns mathematical proofs into verifiable computer programs, it fit naturally into the kind of work she was already doing. It was less a new direction than a new tool for an old obsession.
The timing is right because the stakes are rising. AI systems are predictive by design and are writing more software every day in enterprises, often working with domain experts who are less familiar with writing production code. The gap between code that looks right and code that is right is getting wider, harder to identify, and the consequences of getting it wrong are growing. Axiom’s approach, training on formal mathematical proofs and transferring that rigor to code verification, is one of the few technically serious answers to that problem.
Formal verification has historically been expensive, slow, and the province of a small number of specialists. Carina is betting that advances in AI and the maturation of tools like Lean have created a new opening, that you can now build toward provable correctness at scale, not just in isolated systems but across complex, real-world software that breaks in unpredictable ways. In December, AxiomProver achieved a perfect score on the Putnam Exam and, more recently, demonstrated that those reasoning skills carry over to code verification benchmarks as well.
We’ve been close to Carina and the Axiom team since our day one investment in the seed round, and we’ve had a front-row seat to how she builds. She’s unusually rigorous, determined, and objective about what the work requires for success. She understands that the problems worth solving don’t yield to brute force alone, that the founders who win in spaces like this are the ones who can hold a long-term architectural vision while making the right near-term calls on use cases and go-to-market partners. On both counts, she’s world class, and her pace of learning has only accelerated.
Madrona is proud to continue supporting Axiom as they go after one of the most important unsolved problems in applied AI. Congratulations to Carina, Shubho, and the whole team.
Related Insights
