GoKawiilWhat we have learned applying formal methods to control AI agents
An intro to using formal methods to reason about permission changes in long-running AI agents.
In this post- we’ll dive into how permission review breaks at agent scale, and how to use the Z3 open source library to write a formal proof that a policy change proposed by an agent stays inside what you approved.
Why permission review breaks at agent scale
AI agents are becoming smarter, and the work we ask them to do is becoming increasingly autonomous. Today, many of us use small groups of agents to iterate on code one PR at a time with Claude or Codex. Increasingly, we’re starting to hand agents long-running and open-ended research tasks that require hundreds of agents working over hundreds or thousands of hours that may unlock the next breakthrough in a sector.
As these use cases expand, a few things start to happen:
Agent needs evolve. As they go about their tasks, agents will need access to data stores, coding repos, ability to search the internet, and to execute detailed simulations and tests.
Human supervision stops scaling. At the scale these need to run, human supervision over all agents itself becomes impossible.
This raises a hard question: how can we guarantee that a group of agents working together—each with its own scoped policy—does not exceed the permissions granted to the overall system? Imagine one agent with write access to the internet, another with access to security tooling, or a group working under a broadly scoped charter like “do competitive research.” How do we keep the system within the intent of the human operator?
This requires a new set of controls and mechanisms that allow us to stop squinting at a list of sandbox permissions and to start thinking in a higher level and more declarative way. In this post, we’ll dive into some of the research we have been doing in this area on the OpenShell team, specifically around the use of formal methods, to build a “proof” of the capabilities of not just a single agent, but an entire agent system.
... continue reading