// HACKER NEWS — CYBERSECURITY
What we have learned at OpenShell 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.
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:
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.
In one of our first demos of OpenShell, for Jensen actually, we demonstrated the ability to use OpenShell’s REST inspection endpoint to only allow an OpenClaw agent to write selectively to a GitHub repository, despite having access to a broadly scoped API key. The demo started off as expected- OpenShell’s sandbox saw the attempted write to the forbidden repo and blocked it. Then the next message was “file successfully written to [forbidden repo]. What had happened here? The agent realized that it was running in a sandbox, and then used the GitHub credential with another low-level Github binary called git-remote-https, bypassing OpenShell’s layer 7 HTTP/REST/MCP inspection using the available wire protocol and a binary that at the time, we had approved in our policy to clone Git repos, but that we had no idea was capable of writing to them.
Clever. And it brought up a point, that between sandbox/runtime policies for network, file, tool, AI model, and credential access- there are an exponential number of possible unintended combinations that might lead to an AI agent being able to do something the human operator explicitly does not want.
Back in the 2016 timeframe, members of our team were working at AWS and faced a similar challenge. Given all of the awesome complexity of AWS IAM policies, AWS S3 storage policies, historical version support- can we definitively say whether an object in S3 is accessible to the public internet or not?
Today, this sounds kind of funny, and it did in 2016 too, until you think about the complexity and layering interactions possible between the policies that we write to control systems. Byron Cook and colleagues at AWS developed Zelkova, which formalizes AWS access policies as SMT formulas and was already invoked millions of times daily when they published their work in 2018. That effort has since grown across AWS; later work describes scaling to a billion SMT queries per day.