Full episode · 21 min
One Bug Fixes Most C Code Vulnerabilities | Tudor Achim
Tudor Achim argues that formal verification can eliminate classes of software vulnerabilities and is urgent for critical systems as AI speeds up attacks.
MTS · Sophia Dew
- Tudor Achim is cofounder and CEO of Harmonic.
The best minutes
- 2:41Formal verification proves specific bug classes are absent4 min
- 6:24C code becomes verifiable by modeling its operations in math3 min
- 13:09Critical infrastructure faces bridge-scale cybersecurity risk3 min
Also worth watching
Skip the opening introduction, the Lovable sponsor read, and the closing sponsor reads.
Summary · 2 min read
Tudor Achim is the cofounder and CEO of Harmonic. He leads work on Aristotle, which Harmonic expanded from mathematical proofs to verifying C code and chip designs.
Achim says Aristotle turns code behavior into mathematical models that computers can check, enabling formal verification of C code and chip designs. He argues this can rule out defined classes of vulnerabilities, such as memory-safety errors, while AI bug-finding alone cannot prove that a search is complete. He says verification makes most sense where failures could threaten lives, finances or cybersecurity, rather than for every piece of software. He warns that AI-enabled attacks raise the stakes for critical infrastructure and says governments and companies are moving to address the risk.
Minute by minute
- 0:55Aristotle brings verification to C
Achim says Aristotle is, to his knowledge, the first generally available product able to verify C code and hardware designs at large scales. He says it extends verification to existing software by compiling code to Lean, where a computer can check its logic.
- 2:41Formal checks reduce exploit vectors
Achim says formal verification cannot prevent every hack: code can behave as specified and still run with a weak password. But he argues that proving properties such as memory safety can remove a common starting point for exploits. He cites Heartbleed as an example and says Aristotle would have caught it.
- 5:09Formal verification gives a stopping point
Achim distinguishes bug-finding tools, including powerful AI, from formal verification: a search that finds no issue cannot prove that a class of bugs is absent. For specified properties such as memory safety or some privilege-escalation issues, he says formal verification checks all possible cases, while a deterministic program checks the reasoning.
- 6:24C and chip logic becomes math
Achim says Aristotle models operations such as memory access and arithmetic mathematically, then combines those models to describe what the code does. He says C and Verilog are difficult to model, and a useful verification product must be correct, capable at scale, fast and reasonably priced. He says Aristotle is getting faster and cheaper and adding languages.
- 10:22Verification depends on failure costs
Achim says blanket verification is not economical for every system: a service that can simply restart may not justify the cost, and companies will choose their level of assurance. He recommends verification when failures could threaten lives, finances or cybersecurity. He points to airplane software and chip designs, where a tape-out failure can cost hundreds of millions of dollars or more at TSMC.
- 12:13AI raises risks to critical infrastructure
Achim confirms Harmonic is working with governments but shares no specifics. He argues that democracies need to protect systems such as electric grids and air-traffic control from AI-enabled attacks, because the software was not designed for sustained, large-scale intelligent attacks. He compares the risk to finding critical defects in every bridge and says software is easier to fix.
- 15:27Companies are moving on security
Achim says formal verification can show that a more secure rewrite preserves the old code's behavior. He says CVEs are being discovered at a high rate and CISOs recognize the risk. He cites JP Morgan as an early user of tools such as Mythos to resolve bugs, and says companies can act on their own, though government rollouts require coordination.
Published Oct 31, 2026.
Transcript · 17 min read
MTS, hosted by Sophia Dew, with Tudor Achim.
Transcribed by machine (Whisper) from the episode’s audio, so a word may be off here and there.
a lot of exploits in really security-sensitive code, like C code, chains together these things called memory exploits, where the programmer allows for some behavior that was not intended, like writing to some memory you don't own or using some data after you technically had permission to use it, and then combining memory exploits with things like privilege escalation, other bad behavior. If you can completely get rid of that first class of issues, like memory safety issues, you actually limited a lot of vectors for hacks. And so that's one way in which verifying your code can reduce your risk of security breaches.
Hello, everyone. Welcome back to MTS. Today, we are joined by Tudor Akeem, the co-founder and CEO of Harmonic, which this week expanded its Aristotle system for math proofs to verifying C code and chip designs. Tudor, welcome to MTS. Hi, nice to meet you. Thanks for having me. Great to have you on. I know you guys had a big week this week. You guys went viral as well, all on X. Tell us a little bit about what you guys announced. Yeah, yeah. Aristotle, I think, to my knowledge, is the first product available that's generally available that can verify all sorts of C code, hardware designs at very large scales.
And we just think this is really important in this new generation of cybersecurity where it seems like everyone's getting hacked all the time because humans wrote a lot of code that had a lot of problems. So now you can kind of check it, make sure it's right. And the code you write in the future, you're really guaranteed to not have certain classes of issues that code of the past did. Yeah. So for people who are not familiar, what exactly is verifiability and why is that important in our code? Yeah. When you verify code, you can think of it as stepping logically through it like you would in your head but in a way you can check with the computer so when you're a programmer when programmers used to write code by hand you'd have some idea of what the code assumes and then you kind of step through it in your head you say okay well if i have these assumptions on the input then my code that i wrote it can only do so many things so i can prove something about the output and you do that in your head when you verify code with the computer you do that same process except instead of all that logic living in a developer's head the computer writes it out in the computer language and another computer program checks it. So code is verifiable if you
Read the whole transcript
can check the logic with the computer in that way. Historically, a lot of code has not been verifiable. People had to create new languages to verify it, like Lean, which I think is the best interactive theorem prover. But now if you can compile existing code, existing software code to Lean, now all of a sudden existing software code becomes verifiable as well. And that's
“But let's say you run an AI system to try to find a bug in your code base and it says, I haven't found a bug.”
“So you'd say, okay, well, I access the memory. Okay, let's build a mathematical model of that.”
But what's next for you guys?
What can people expect to see over the next few months? Well, the system is getting faster and cheaper every day. We have a lot of new languages coming that we're excited about. I just think it's really important that all of the world's safety critical code gets verified, whether through Aristotle, which is available through other means. I think without that, it's kind of an unforced error. You know, if you have memory safety issues lying around, five years ago, okay, it takes a very special human to find it. But these days with AI, it's so easy to find them that you're kind of a sitting duck if you don't verify.
So I think besides just adding more languages and features, we're just excited to bring it to the masses and make sure that, you know, what people used to think was an impossible task to formally verify their real code base is now actually pretty tractable and pretty easy to do. I want to shout out our sponsor, Lovable. You know the app you've been meaning to build? The internal tool, side project, or product you'd otherwise lose a weekend to? With Lovable, you get software you can ship today. That includes an editable codebase you can inspect and change, plus two-way GitHub sync. Lovable also handles the backend and infrastructure, including managed Postgres, auth, storage, hosting, payments, and more, so you don't have to wire it all up yourself.
And through Lovable's MCP server, you can create and deploy your project directly from the agents you already use. turn ideas into software people love with lovable lovable.dev now on to the episode
“if the worst thing that happens to your code is you just restart your web server, maybe you don't have to verify it.”
You're seeing the superintelligence task force in the White House, a lot of these different orgs that are recognizing that the future of AI, the future of superintelligence is a national security issue. These are things that countries all around the world are taking more seriously about their systems. And so curious to get your perspective as you guys are working on Aristotle, working on actually making code verifiable.
Are you also working with governments, too, on getting this implemented in critical infrastructure? Yes, we are. Yeah, yeah. Also, yeah, if you look at. Yeah, we are. Anything you can share more about? Okay, fair. Awesome. I figured I was just trying to see, you know, any little stuff you can actually share. But in terms of what you can share, maybe just at a high level, why is that important to work with governments?
“I would say that the cybersecurity risk to national infrastructure is about as bad as having damage in every bridge in the country.”
How is that actually showing up? I think this is a broader trend that I think people can also see on Twitter. I think the rate of CVEs being discovered is just unbelievable at this point. I think anybody who's serious in cybersecurity is aware and moving quickly and all the CISOs we talk to, they're usually on the ball about the risk. Yeah. One thing I want to get your perspective on, especially when it comes to chief security officers at different companies, typically, right? I mean, it's companies, you're competing, but when it comes to security and cybersecurity, I'm seeing people from all different companies, even competing companies come together to try to figure this out. What are you noticing as well?
I think that people understand the danger. I'll just put it that way. I think that there will have to be a lot of coordination to bring all these technologies into governments, for example. But I do think that within companies, they're pretty efficient. So, you know, if you talk to most CISOs, they'll understand the ROI of various technologies for securing themselves. I think companies like JP Morgan were pretty early in using technologies like Mythos internally to resolve bugs. So I think that there needs to be some coordination, but everyone seems to be figuring pretty good things out on their own.
I think that it's not the case that if you don't coordinate, you're lost. I think that, you know, the technology exists, you can just apply it and secure yourself. Super fascinating. I mean, that's great to hear. It's not like the bridge analogy in terms of the logistics to make this happen is going to be a national emergency wide scale thing. This is something that can be easily fixed. Tudor, really wanted to thank you for joining us today on MTS, sharing all about Aristotle, the latest informal verification, how this can become mainstream, how this can be easily used within our code to harden and secure all of our critical infrastructure.
Super important stuff. So thank you so much for joining us today on MTS. Thanks so much for having me, Sophia. A huge thanks to MTS sponsors. 11 Labs, AI that communicates at human level across every channel and modality. 11labs.io slash MTS. scale your startup on neon millions of developers and startups have already chosen neon for their back end start on the free plan or get up to a hundred thousand dollars in credits for your startup at neon.com slash mts special thanks to our sponsor kong the ai connectivity platform connect apis llms agents and systems with serious security and governance konghq.com finally prove what your ai investment is worth with lairdan head to lairdan.com today to start measuring your AI's bottom line. MongoDB, trusted to run critical applications by 75% of the Fortune 100, the intelligent data platform for the era. Apply today for access to up to $15,000 in Atlas credits, dedicated technical support, and exclusive events and go-to-market opportunities.
MongoDB.com. Chargebee, billing and monetization infrastructure for the AI era. Chargebee.com. support for the show comes from vcx the public ticker for private tech the u.s stock market started history's greatest wave of wealth creation From factory workers in Detroit to farmers in Omaha, anyone could own a piece of the great American companies. But today, our most innovative companies are staying private longer, which means everyday Americans are missing out. Until now. Introducing VCX, a public ticker for private tech. Visit GetVCX.com for more info. That's GetVCX.com. Carefully consider the investment material before investing, including objectives, risk, charges, and expenses.
This and other information can be found in the innovations fund prospectus at getvcx.com. This is a paid sponsorship.
