# C code becomes verifiable by modeling its operations in math

Markdown copy of https://realalpha.app/s/c-code-becomes-verifiable-by-modeling-its-operations-in-math/ on Real Alpha, the best minutes from long interviews with the people building AI. Cite and link the page, not this copy.

- Speaker: [Tudor Achim](https://realalpha.app/people/tudor-achim/) · Tudor Achim is cofounder and CEO of Harmonic.
- Host: [Theo Jaffee](https://realalpha.app/people/theo-jaffee/) · Co-founder & host, MTS · One of the first members of a16z's new media team; earlier hosted the Emergent Ventures-backed Theo Jaffee Podcast.
- Host: [Sophia Dew](https://realalpha.app/people/sophia-dew/) · Host, MTS
- Show: MTS
- Episode: [One Bug Fixes Most C Code Vulnerabilities | Tudor Achim](https://realalpha.app/v/FSsg2i4yF_Y/), Oct 31, 2026
- Moment: 6:24 to 9:01 of the episode (3 min), playing on https://realalpha.app/s/c-code-becomes-verifiable-by-modeling-its-operations-in-math/; the episode from there: https://realalpha.app/v/FSsg2i4yF_Y/?t=384

## Quote

> “So you'd say, okay, well, I access the memory. Okay, let's build a **mathematical model of that**.”
> — [Tudor Achim](https://realalpha.app/people/tudor-achim/) at [7:00](https://realalpha.app/v/FSsg2i4yF_Y/?t=420) · MTS

## Takeaways

1. Modeling each operation creates a mathematical account of what code does.
2. C and Verilog are difficult to model precisely.
3. Verification must be correct, capable, fast and affordable.

## About this segment

Aristotle models C operations such as memory access and arithmetic as mathematical steps. Tudor Achim says a useful verification product must balance correctness, scale, speed and cost.

From “One Bug Fixes Most C Code Vulnerabilities | Tudor Achim”, Oct 31, 2026. [Watch the full episode](https://realalpha.app/v/FSsg2i4yF_Y/)

## Transcript

Transcribed by machine (Whisper) from the episode’s audio, so a word may be off here and there.

[6:27](https://realalpha.app/v/FSsg2i4yF_Y/?t=387) 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, it's nothing. It's not black magic. You're just looking at the code and you're just saying very 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 addition. Let's build a mathematical model of what that does. And if you chain together these

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

[7:37](https://realalpha.app/v/FSsg2i4yF_Y/?t=457) 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. The first one is that it's correct.

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

[8:53](https://realalpha.app/v/FSsg2i4yF_Y/?t=533) But what's next? So I know this is just like one aspect and what you guys announced this week was pretty novel.