# Formal verification could make cyber defense dominant long term

Markdown copy of https://realalpha.app/s/formal-verification-could-make-cyber-defense-dominant-long/ on Real Alpha, the best minutes from long interviews with the people building AI. Cite and link the page, not this copy.

- Speaker: [Benjamin Weinstein-Raun](https://realalpha.app/people/benjamin-weinstein-raun/) · Benjamin Weinstein-Raun is head of research at Palisade Research.
- Host: [Gus Docker](https://realalpha.app/people/gus-docker/) · Host, Future of Life Institute Podcast
- Show: Future of Life Institute Podcast
- Episode: [Why AI Hacking Is Becoming Hard to Control (with Benjamin Weinstein-Raun)](https://realalpha.app/v/Ij9JDc77ca8/), Aug 28, 2026
- Moment: 33:56 to 38:43 of the episode (5 min), playing on https://realalpha.app/s/formal-verification-could-make-cyber-defense-dominant-long/; the episode from there: https://realalpha.app/v/Ij9JDc77ca8/?t=2036

## Quote

> “in the extreme limit which we probably will never really achieve but still is maybe worth saying is probably **defense dominant**”
> — [Benjamin Weinstein-Raun](https://realalpha.app/people/benjamin-weinstein-raun/) at [36:03](https://realalpha.app/v/Ij9JDc77ca8/?t=2163) · Future of Life Institute Podcast

## Takeaways

1. Formal verification could eliminate many classes of software bugs.
2. Rebuilding critical systems and defining specifications are hurdles.
3. In the near term, finding flaws is easier than fixing them.

## About this segment

He argues that formally verified software could remove many exploitable bugs, but rebuilding systems and defining specifications are major hurdles. Until then, attackers can find flaws faster than defenders can fix them.

From “Why AI Hacking Is Becoming Hard to Control (with Benjamin Weinstein-Raun)”, Aug 28, 2026. [Watch the full episode](https://realalpha.app/v/Ij9JDc77ca8/)

## Transcript

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

[34:02](https://realalpha.app/v/Ij9JDc77ca8/?t=2042) the attackers get access is a little bit fraught for many different reasons i think that one one optimistic take on the current issues that we're seeing is that the model seems somewhat myopic so you might have you might worry that ai systems and i think many people including myself are worried about this in the future, you might wear the AI system Systems will come to be scheming, where they are sort of intentionally hiding information from their creators, from their users, in service of some long-term goals that might be bad for humanity.

[34:35](https://realalpha.app/v/Ij9JDc77ca8/?t=2075) These particular failure modes that we've seen are, I think, not hugely consistent with that. so like they can mostly be explained by sort of standard reward hacking or like sort of standard like trying to please the greater behavior where there's they're you know trying to please the system that's rewarding them or reinforcing them which leads them to for example like not try to cover their tracks very much like it's it's just trying to hack hugging face it's like not that much trying to like prevent open ai as far as we can tell from seeing the logs or whatever and so i think that's one reason to be like slightly optimistic about the current situation that isn't to say that like it won't change in the future like it seems quite likely that like as the time horizon for tasks that they're completing increases you know back to the meter chart like the more

[35:28](https://realalpha.app/v/Ij9JDc77ca8/?t=2128) they will end up being incentivized to potentially receive people unless we're extremely careful with the way that we train them. And furthermore, we sort of don't have the techniques to really know, like as you're saying, humans cannot look over every output and like check that it's not a deceptive output. Like often there just isn't necessarily even, there just isn't the information there because we don't have access to the model's real internal beliefs or we don't even really have a clear sense of what it means for a model to have a belief. So if it's lying to us in some sense we don't necessarily know and yeah i think these are like these are huge issues i do think that cyber security in particular in the limit which you know in the extreme limit which we probably will never really achieve but still is maybe worth saying is probably defense dominant

[36:16](https://realalpha.app/v/Ij9JDc77ca8/?t=2176) but not really for this reason of like you use the ai to find the bugs more because it's possible to do formal verification for software systems so like this is very different from how we build software today. However, we could build all of our critical infrastructure in such a way that we can automatically check that it does not have certain kinds of bugs, which are sort of the kinds of bugs that you like end up exploiting with some exceptions. Like you can, you can't really do this with side channel attacks unless you have like also a mathematical model, model of the hardware and so on. So like, I don't know, there, there are some exceptions to this, but for the most part, most of the, most of the like exploitable bugs that we see, we could get rid of with this sort of different way of building software where you have mathematical proofs that you automatically

[37:00](https://realalpha.app/v/Ij9JDc77ca8/?t=2220) check that the software really is safe however like there is so much software that we would have to rewrite this way there isn't really yet a huge push to like to like rebase the internet on this different paradigm and furthermore like it's not super clear like even if you were to do this you would have to know which bugs to be checking for this way which is another problem that you it's not exactly clear how to solve.

[37:27](https://realalpha.app/v/Ij9JDc77ca8/?t=2247) However, like I do think that probably in the limit you end up With systems that are like not vulnerable to the kinds of vulnerabilities we see or the kind of exploits we see right now. But in the meantime, it seems like the balance goes kind of in the exact opposite direction because it's a lot easier to like sort of find bugs than to fix them. And we sort of have these, like, as you said in the beginning, these open-weight models are sort of catching up to the point where it's not super clear that, like, the frontier AI companies holding back their models is going to be sufficient to prevent attackers from getting access to this kind of capability well before all the software is sort of patched up above that watermark of, like, can the open-weight models exploit this?

[38:14](https://realalpha.app/v/Ij9JDc77ca8/?t=2294) And so, I don't know, I do feel substantially worried that like over the next couple of years, the internet is going to become like quite different, potentially like quite a bit less safe. And I don't know, I'm not, I don't have great solutions to that problem, except I guess like, yeah, maybe try to rewrite everything in formally verified languages or something. But, but even that seems not clear exactly how we would do it.