Announcing Formal Verification at RESI (The Institute for Responsible Superintelligence)

This post is crossposted from my Substack, Structure and Guarantees , where I explore how formal verification and related ideas might scale to more complex intelligent systems. This article is a little different from usual: it’s an announcement of a new working group studying how to get formal methods off the ground, for pervasive use to address current concerns around cybersecurity and AI coding agents (and beyond). There’s a lot of excitement and worry at the moment about OpenAI agents hacking into Hugging Face , as an example of increasingly powerful AI creating cybersecurity threats that feel fundamentally new. I’ve already written about how there are actually new opportunities we should seize for defenders , so the balance of power need not shift in favor of the bad guys. Formal verification is a secret weapon whose time has come. It even gives some important security theorems almost for free ! In the case of that recent OpenAI-Hugging Face incident, a relevant application would be provably enforced containment (a case of guaranteed safe AI ), whether within an evaluation environment or a production system. This kind of theorem can promote safety independently of what goes on within mysterious decision-making black boxes like deep neural networks. I’m excited to announce here a new initiative to figure out the contours of an effort to ramp up related formal-methods work quickly and effectively. RESI, the Institute for Responsible Superintelligence , was recently kicked…