# One Bug Fixes Most C Code Vulnerabilities | Tudor Achim

Markdown copy of https://realalpha.app/v/FSsg2i4yF_Y/ on Real Alpha, the best minutes from long interviews with the people building AI. Cite and link the page, not this copy.

Tudor Achim argues that formal verification can eliminate classes of software vulnerabilities and is urgent for critical systems as AI speeds up attacks.

- Show: MTS
- Hosts: [Sophia Dew](https://realalpha.app/people/sophia-dew/)
- Guest: [Tudor Achim](https://realalpha.app/people/tudor-achim/) is cofounder and CEO of Harmonic.
- Published: Oct 31, 2026
- Length: 21 min

## The best minutes

- [2:41](https://realalpha.app/v/FSsg2i4yF_Y/?t=161) [Formal verification proves specific bug classes are absent](https://realalpha.app/s/formal-verification-proves-specific-bug-classes-are-absent/) (4 min)
- [6:24](https://realalpha.app/v/FSsg2i4yF_Y/?t=384) [C code becomes verifiable by modeling its operations in math](https://realalpha.app/s/c-code-becomes-verifiable-by-modeling-its-operations-in-math/) (3 min)
- [13:09](https://realalpha.app/v/FSsg2i4yF_Y/?t=789) [Critical infrastructure faces bridge-scale cybersecurity risk](https://realalpha.app/s/critical-infrastructure-faces-bridge-scale-cybersecurity/) (3 min)

## Also worth watching

- [10:22](https://realalpha.app/v/FSsg2i4yF_Y/?t=622) [Verification should match the cost of a failure](https://realalpha.app/s/verification-should-match-the-cost-of-a-failure/) (2 min)

Skip the opening introduction, the Lovable sponsor read, and the closing sponsor reads.

## Summary

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:55](https://realalpha.app/v/FSsg2i4yF_Y/?t=55) **Aristotle 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:41](https://realalpha.app/v/FSsg2i4yF_Y/?t=161) **Formal 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:09](https://realalpha.app/v/FSsg2i4yF_Y/?t=309) **Formal 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:24](https://realalpha.app/v/FSsg2i4yF_Y/?t=384) **C 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:22](https://realalpha.app/v/FSsg2i4yF_Y/?t=622) **Verification 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:13](https://realalpha.app/v/FSsg2i4yF_Y/?t=733) **AI 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:27](https://realalpha.app/v/FSsg2i4yF_Y/?t=927) **Companies 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.

## Transcript

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.

[0:00](https://realalpha.app/v/FSsg2i4yF_Y/?t=0) 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.

[0:37](https://realalpha.app/v/FSsg2i4yF_Y/?t=37) 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.

[1:17](https://realalpha.app/v/FSsg2i4yF_Y/?t=77) 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

[2:21](https://realalpha.app/v/FSsg2i4yF_Y/?t=141) 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 exactly what Aristotle does. So when things are more verifiable, explain how that prevents hacks. Well, it doesn't prevent all hacks. So I think there's a meme on Twitter that, you know, verifying everything prevents all bugs. You can imagine verifying code just means that you're 100% sure the code does what it says it does. So if you formally verified some code, like a web server, and then you run it with a configuration that says the password to it is password, you're going to get hacked no matter how verified that code is but but it turns out 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

[3:36](https://realalpha.app/v/FSsg2i4yF_Y/?t=216) exploits with things like privilege escalation other bad behavior if you can completely get rid to 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. If we're thinking of a specific example, for example, the Binance theft, this is 6.3. three billion dollars is one of the probably the biggest crypto hack ever to date can aristotle help out here is there anything that aristotle could have done to rule it out and prevent this attack well i think that one happened yesterday so i don't know if anyone knows exactly outside of binance knows exactly what happened there um we do have some security related things we've discovered in very popular open source systems that we're gonna work with the maintainers to fix and those we know we've prevented hacks also if you just look back at the history of hacks i mean there was this hugely popular one called or famous one called heart bleed do you remember that yeah yeah heart bleed was a classic memory safety issue and if you had run aerosol on the code you of course would have caught it and then fixed it ahead of time yeah so tell us a little bit about

[4:49](https://realalpha.app/v/FSsg2i4yF_Y/?t=289) this i mean right now you have ai is now running a lot of these verifications itself and you have like AI actually verifying its own output. But that's not always that reliable. It's not always 100% verifiable in that way. And so tell us a little bit about what are the other systems that people are using for verification and why that's not something that can scale into what we need now. Yeah, I think the biggest conceptual difference is that for 40 years in software engineering, what we've been getting better at is bug finding. So you used to have humans find bugs and then they find security bugs. And now these latest AI systems that are really, really powerful, still what they're doing is finding bugs. But the thing is, if you have a really powerful AI system that finds bugs, you don't really know when you're done. So you can always run it more and see if it

[5:41](https://realalpha.app/v/FSsg2i4yF_Y/?t=341) **Tudor Achim:** finds some other bug. 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. You can't really be 100% sure that you've ruled out an entire class

[5:50](https://realalpha.app/v/FSsg2i4yF_Y/?t=350) of bugs. That's where formal verification is a bit different. When it comes to certain classes of errors, like the memory safety one, like certain privilege escalation issues, with formal verification, you get a checkmark that you've actually analyzed all the possible bugs that could arise and you prove that none exist. So that's one way in which it's different. You know when you're done. And the other way in which it's different is what I mentioned before, which is that here you have a formal system that's checking the AI reasoning. So it is a computer tool, but it's not a non-deterministic one like AI. It's one that really just runs an algorithm that's very simple and checks reasoning step by step. Yeah. And it also just comes to actually doing verification, lean and math proofs. That's one of the main fundamental ways, but that's great for math. You guys are working right now with verifying C code, chip designs. How is this possible? I know this is one of the first actually systems of its kind, but what is possible? What's unique about C code chip designs that makes it verifiable through the system? Well, we actually went with hard mode. I think these are actually two very hard languages to model in math. But really,

[6:55](https://realalpha.app/v/FSsg2i4yF_Y/?t=415) it's nothing. It's not black magic. You're just looking at the code and you're just saying very

[6:59](https://realalpha.app/v/FSsg2i4yF_Y/?t=419) **Tudor Achim:** precisely, what's a mental model of what happens when I run one step of this C code? So you'd say, okay, well, I access the memory. Okay, let's build a mathematical model of that. And then you do some

[7:09](https://realalpha.app/v/FSsg2i4yF_Y/?t=429) addition. Let's build a mathematical model of what that does. And if you chain together these mathematical models of what it means to access memory, to do arithmetic, to write things to memory, to read things from devices, all of a sudden you have a pure mathematical model of what the code does. So that's what makes it verifiable. It doesn't mean it's easy to build these models. There's a lot of details about how C works, how Verilog works. Some of these languages don't even have formal definitions of what it means to be a certain language feature. but once you build that mental model in math it's now a math problem just like all the other problems we trained Aristotle to solve as you guys were actually building this out what was the hardest part oh man where do I begin I think uh I think that it's very hard to make a system that's great for people to use so there's four things you that matter in a formal verification product.

[8:01](https://realalpha.app/v/FSsg2i4yF_Y/?t=481) The first one is that it's correct. No matter what else you do, if you prove something that's actually false, that's the worst thing possible. The second thing is that it should be capable. So it's easy to build kind of a toy example where you verify a very short piece of code, but then when you want to verify an entire chip, the whole thing breaks down. The third thing is latency. So people were used to not having any formal verification tools, but as soon as we work with a lot of design partners, as soon as you give them a tool, they get used to it working very quickly and now they want it to be really fast.

[8:30](https://realalpha.app/v/FSsg2i4yF_Y/?t=510) And then the very last thing that matters is cost. So there are huge challenges across all these areas. How do you make sure your compiler is correct? How do you make sure it can really scale to huge designs? How do you make sure it's fast? And how do you make sure that with all they're keeping the cost reasonable? So there's a lot of challenges the team has overcome and I'm really proud of them, but I wouldn't call it just one area that's kind of hard across the board. But what's next? So I know this is just like one aspect and what you guys announced this week was pretty novel. But what's next for you guys?

[9:01](https://realalpha.app/v/FSsg2i4yF_Y/?t=541) 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.

[9:34](https://realalpha.app/v/FSsg2i4yF_Y/?t=574) 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.

[10:13](https://realalpha.app/v/FSsg2i4yF_Y/?t=613) 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 do you see the future of for example right now most code that is written is ai generated do you see the future is just going to be ai not only writing the code but also verifying the code when it's publishing it i think that there it's a little more subtle than that i think that there's this meme on Twitter right now that all code, you know, must be verified. You know, our mission is

[10:49](https://realalpha.app/v/FSsg2i4yF_Y/?t=649) **Tudor Achim:** to verify all software. But the reality is if the worst thing that happens to your code is you just restart your web server, maybe you don't have to verify it. Maybe the ROI isn't there. In the same

[10:57](https://realalpha.app/v/FSsg2i4yF_Y/?t=657) way, if you look at some of the recent results of verifying binary code, that's a very expensive way to check code. And almost all security vulnerabilities come from human error, not compiler error. So I think actually the future is more nuanced. I think companies will determine how much they're willing to pay for verification to what level they want that level, to what level they want the assurance. And there's gonna be a lot of products that span that. It's not just gonna be a black or white, you know, either you verified your code and it's right or it's not verified and it's totally wrong. Yeah, and exactly what you mentioned for some of these companies, the worst thing that happens is the page reloads.

[11:31](https://realalpha.app/v/FSsg2i4yF_Y/?t=691) What are the specific types of use cases, companies, industries that you think it's essential that they're verifying their code? Well, as a consumer who flies on airplanes, I'd love for plain software to be verified, you know. Well, great point there. I think we should expect any piece of software that, you know, might cause danger to human life or finances or cybersecurity. I think it's got to be verified. And then if you go to chip. I mean, people that are building inference chips, training chips, etc. If you have a tape out failure, you're paying hundreds of millions of dollars to TSMC, if not more.

[12:07](https://realalpha.app/v/FSsg2i4yF_Y/?t=727) So I think in these areas, you know, again, where the cost of failure is a lot more than just restarting a server, you're probably going to want to verify the code. Yeah, it's pretty interesting right now. 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.

[12:39](https://realalpha.app/v/FSsg2i4yF_Y/?t=759) 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? Well, I think that, you know, we work with democracies. And I think that with the wide availability of AI that's offensively capable, the software that powers things like the electric grid or air traffic control or these systems.

[13:29](https://realalpha.app/v/FSsg2i4yF_Y/?t=809) I mean, it's hard to drive home maybe to Twitter viewers like how important this stuff is, but this software was not designed to withstand sustained at-scale use of intelligent AI to attack it. I think that if we don't fix the code quickly and automatically and in an airtight way, you're basically guaranteed to enable adversarial actors to exploit those bugs and you put a lot of the country at risk. So I just think it's a matter of time. It's kind of when, not if you verify all the critical code. And I think it's good that governments are paying attention to it. You brought up a really important point. Maybe the mainstream person on X when they're scrolling doesn't totally realize how close we are to things not working like critical infrastructure like our power grid you mentioned or air like supply chain whatever that might be and so if you're communicating straight to the audience right now straight to people on x make the case why is this important i'm going to borrow an analogy that um an ex-secretary of defense told me so the analogy is i think the world of cybersecurity right now is imagine if every bridge in America we discovered that had some critical defect in the materials used to make it. So there's a problem with the concrete and it has

[14:55](https://realalpha.app/v/FSsg2i4yF_Y/?t=895) really bad cracks after some amount of time. We basically have to replace all those bridges immediately. And if you face that kind of problem in a society, this isn't the kind of thing where you're like, oh, it's kind of expensive. Let's just do it later. You kind of have to do it right

[15:06](https://realalpha.app/v/FSsg2i4yF_Y/?t=906) **Tudor Achim:** now. I would say that the cybersecurity risk to national infrastructure is about as bad as having damage in every bridge in the country. That's like the scale of the problem. So that's

[15:19](https://realalpha.app/v/FSsg2i4yF_Y/?t=919) how I drive it home. And yet when it comes to a bridge, it's a huge human logistics problem. We have to figure out how to get the concrete and the materials. This is easier to fix. This is easier to fix. So do you have any estimates here on timelines? What is the urgency that's actually happening maybe amongst governments and these systems will the timeline by this time next year do you think all of our infrastructure will be a lot more hardened a lot more secure or do you think by a year from now we're going to be feeling this problem more than ever before i think a lot of problems will be addressed i think that people are moving quickly also with tools like aristotle i mean the problem is if if you try to rewrite your code in a way that's not verified, you don't really know that you did it right. With Aristotle, you're guaranteed that the behavior is the same. Sorry, with formal verification in general, you can verify that anything that happens in the old version of the code happens in the new one, but it's more secure with memory safety or whatever. So I think that unlike a year ago, the technology now exists to be able to do all these giant rewrites, make everything safe. So I think that people understand the danger and will apply the

[16:26](https://realalpha.app/v/FSsg2i4yF_Y/?t=986) technology. Yeah. Are you seeing that urgency as well within companies, within other countries? 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?

[17:18](https://realalpha.app/v/FSsg2i4yF_Y/?t=1038) 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.

[17:55](https://realalpha.app/v/FSsg2i4yF_Y/?t=1075) 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.

[18:32](https://realalpha.app/v/FSsg2i4yF_Y/?t=1112) 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.

[19:35](https://realalpha.app/v/FSsg2i4yF_Y/?t=1175) 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.

[20:37](https://realalpha.app/v/FSsg2i4yF_Y/?t=1237) This and other information can be found in the innovations fund prospectus at getvcx.com. This is a paid sponsorship.