Math-Whiz Startups Push A New Way To Check If AI Code Really Works
Startups like the newly-launched Logical Intelligence, and the Robinhood CEO's new venture Harmonic, are pushing math-heavy "formal verification" models to secure AI code.
In ‘The Martian,’ Andy Weir’s sci-fi novel that became a popular film starring Matt Damon ten years ago (I had to double-check that to believe it), stranded astronaut Mark Watney utters a much-repeated line:
“In the face of overwhelming odds, I’m left with only one option: I’m going to have to science the shit out of this.”
It’s a good line! Astrophysicist Neil deGrasse Tyson loved it. And it pops into mind as Upstarts talks with Eve Bodnia, a mathematician turned startup founder, earlier this week.
Pacing outside the Center of Mathematical Sciences and Applications, a research center at Harvard University where she and some of her team were hosting a dinner with Meta’s Yann LeCun, Bodnia explains a current problem with generative AI and the large language models you know about by now from Anthropic, OpenAI, xAI and the rest: even as models get more powerful, the code they generate is still dangerous for certain use cases.
A new blockchain in crypto handling users’ digital wallets. A health system with patient data. AI-piloted drones or aircraft. Even the inner workings of a cutting-edge microchip. When billions of dollars or lives are on the line, mostly-accurate isn’t enough.
“Pretty much anything that runs on autopilot, you don’t want it to have a mistake,” argues Bodnia. “The current models are too slow, and they hallucinate.”
Her new startup, Logical Intelligence, hopes to solve that problem using a process called “formal verification”. Its model by the same name allows an AI agent, called Aleph, to convert code into mathematical proofs, sometimes tens of thousands of lines long, that can then be verified to what it claims is 100% accuracy, not 99 point something percent. An audit agent called Noa, meanwhile, can run a similar process for bugs in existing code.
Put in plainest terms, Bodnia and her team of prize-winning mathematicians — the staff of 16 include a Fields Medal winner and programming world champion — see your concerns about AI accuracy; their response: we’re going to have to math the shit out of this.
“In the same way as coding AI can scale the number of ‘developers’ in the world 100x, formal math AI could do the same for math research.”
They aren’t the only ones. Robinhood CEO Vlad Tenev, who knows a thing or two about fintech and crypto, co-founded a startup with a similar mission that’s already raised $100 million, called Harmonic. Harmonic’s model, Aristotle, achieved a gold medal performance on the 2025 International Math Olympiad, CEO Tudor Achim has said.
(Achim declined to comment for this story, but Upstarts spoke to several sources about Harmonic’s plans; comment from one of his top backers is below.)
Then there are the big model shops like OpenAI and Google’s DeepMind, which both recently won gold medals of their own. Some AI experts remain skeptical that, as the labs develop better reasoning models, the formal math approaches of Logical Intelligence, Harmonic and the like will be widely needed.
“I doubt that most AI generated code is going to end up formally verified,” says one prominent AI investor.
But these startups are talking to big customers and attracting top talent, and plenty of enthusiasm from other investors. Here’s why.
Keep reading with a 7-day free trial
Subscribe to Upstarts Media to keep reading this post and get 7 days of free access to the full post archives.