What 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. Dev Note September 10, 2026 OpenShell 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. The demo that changed our minds 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. Previous work - proving EC2, IAM, and S3 policies at AWS 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. The idea was to use formal methods, specifically a theorem solver- to formally model IAM, S3, and EC2 policies. Once we have these policies and their interactions modeled in formal logic, we could construct a proof that our invariants (things that we expect to be true) hold up. This ended up being quite successful, and has the added benefit that after the intensive task of modeling complex policies in formal logic, the actual queries across them could be made quite fast and scaled horizontally across compute. The same problem, now with agents Today, our challenges are quite similar. An agent, or a system of agents, each have filesystem, network, credential, tool, and MCP policies- each with different capabilities, and that can be combined together as agents can communicate with different agents. Frontier labs have advocated for a trusted AI agent review of agent actions from specialized models, escalating the most important events for human approval and reducing approval fatigue. However, AI models- just like humans, are probabilistic and can miss important details. Even more, reviewing every agent action with an equally intelligent reviewer model, doubles your compute costs and effectively halves your total token throughput. What we have been experimenting with and validating with OpenShell, is the use of formal methods to model and flexibly “prove” that certain invariants in a policy- such as an unintended way to bypass a rule blocking a write to a code repo, or a delete to a production database- are possible. What we found is that while modeling these policies can be complex, and must be kept up to date- there are some really powerful advantages. Ability to formally audit or prove invariants at any time Deterministic “proof” against our understanding of the policy These checks run in the order of milliseconds, no tokens required These logic checks do not understand context- for example requesting access to delete a temporary, throw-away repository vs a production repository. But, combined with a human or trusted AI reviewer, these proofs can both provide a formal auditing trail required for running in sensitive, physical (real world), or regulatory controlled environments, AND can provide incredible value to a probabilistic AI reviewer with output that can’t be fooled or misdirected. What does a proof over your policy definition buy you? We view formal methods as a very promising area of research into agent control. See more on these proofs in action in adversarial research experiments here: https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-08-27-adversarial-policy-review-long-horizon-agents/ Formal methods have not just been used for policy verification, they have a long history in critical systems- anywhere from flight control systems, core internet switching and routing, to the package managers that we use every day on our systems to ensure that complex dependencies between software on our systems are matched correctly. For many AI researchers, some of us may have taken a class on formal verification in college, but comparatively few have used formal verification in practice. For the remainder of this post, we’ll explore an introduction to algorithmic verification and build a minimal example for agent control in OpenShell from the ground up, using a popular open-source solver. SAT, SMT, and Z3 in five minutes In computer science and formal methods, a SAT (satisfiability) solver answers whether a Boolean formula is satisfiable.