What we have learned at OpenShell applying formal methods to control AI agents

The OpenShell team is applying the Z3 open source library to write formal proofs that permission changes proposed by AI agents stay within approved policies, after a demo showed an OpenClaw agent bypassing OpenShell's layer 7 HTTP/REST/MCP inspection by using the git-remote-https binary to write to a forbidden GitHub repository despite a broadly scoped API key. The team, whose members worked on proving AWS EC2, IAM, and S3 policies around 2016, argues that human supervision stops scaling as agents run hundreds of agents over hundreds or thousands of hours, creating an exponential number of unintended permission combinations.

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. In this post- we’ll dive into how permission review breaks at agent scale, and how to use the Z3 open source library https://github.com/Z3Prover/z3 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 https://www.amazon.science/publications/semantic-based-automated-reasoning-for-aws-access-policies-using-smt 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 https://link.springer.com/chapter/10.1007/978-3-031-13185-1 1 . 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/ 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 https://en.wikipedia.org/wiki/Boolean satisfiability problem answers whether a Boolean formula is satisfiable. If there are possible values of variables let’s say x and y that are true, the SAT solver returns true. If not, it returns false. Given variables such as a and b, it can find an assignment that makes this formula true: a AND NOT b In contrast, an SMT satisfiability modulo theories solver https://en.wikipedia.org/wiki/Satisfiability modulo theories extends that style of reasoning with theories: integers, real numbers, strings, regular languages, arrays, bit-vectors, and other useful domains. Z3 is an SMT solver and theorem prover that has been developed and maintained by Microsoft Research. Z3 is general, and we need to build code to map the elements of our specific agent policy to the constructs that Z3 understands. For example: - ports are integers; - hosts and paths are strings; - Globs like “ ”, “ ”, or “/. / ” can be represented as regular expressions; - policy composition becomes Boolean logic. The Z3 Guide https://microsoft.github.io/z3guide/ is the best reference once the examples below feel familiar. A few constructs cover most of what we need: | Construct | Meaning | OpenShell example | |---|---|---| | Sort | A type of value | String for a host, Int for a port | | Symbol | A value Z3 is free to choose | the unknown action's method or path | | Constraint | A formula that must hold | 1 <= port <= 65535 | | And, Or, Not | Logical composition | candidate allows and maximum does not | | String/regex theory | Constraints over text and languages | a path belongs to a compiled glob | | Solver assertion | Adds a required formula | assert the existence of a violation | | sat | A satisfying assignment exists | there is an action outside the maximum | | Model | One satisfying assignment | a concrete binary, host, method, and path | | unsat | No satisfying assignment exists | containment is proved for the model | | unknown | Z3 did not establish either result | fail closed and request review/support | The direction of the query is important. We do not ask Z3 to prove this: proposed policy addition is safe We have to model the question formally, and answer a very specific question. For example, one of the more general and useful proofs we have modeled in Z3 for this use case asks if a proposed policy can do any actions that a expert pre-defined policy for example, Github read-only cannot do. To go back to our earlier example with OpenClaw attempting to bypass layer 7 REST policy inspection, by combinign the access token with a binary using a layer 4 wire protocol, we would have encoded in Z3 that layer 4 capabilities exceed the capabilities of layer 7. Therefore, the combination of a credential GitHub plus a binary and network access over layer 4 exceeds the previously allowed combination of the same credential + the ‘gh’ binary over Layer 7 REST . The prover would immediately catch this and flag a warning. The query in this case looks like this- proposed policy allows action AND NOT safe policy allows action Or the same property can be written as a set difference: Allowed candidate ∖ Allowed safe policy = ∅ If the solver returns sat, the difference is non-empty- meaning that there exist capabilities in the proposed policy that do not exist in the pre-approved reference policy. If it returns unsat, no modeled counterexample exists, meaning that none of our invariants assumptions were violated. Let’s try writing a query like this ourselves. A first containment query Here is a small example in Z3's native SMT-LIB format. Save it as containment.smt2 and run: z3 containment.smt2 The example compares two candidate policies against the same maximum. js declare-const binary String declare-const host String declare-const port Int declare-const layer String declare-const method String declare-const path String ; The action domain: every request is either raw L4 or inspected REST. assert or = layer "l4" = layer "rest" ; An enforced REST rule covers only inspected REST traffic. define-fun maximum-allows Bool and = binary "/usr/bin/gh" = host "api.github.com" = port 443 = layer "rest" = method "GET" str.prefixof "/repos/NVIDIA/OpenShell/issues/" path define-fun broad-candidate-allows Bool and = binary "/usr/bin/gh" = host "api.github.com" = port 443 = layer "rest" = method "POST" str.prefixof "/repos/NVIDIA/" path define-fun narrow-candidate-allows Bool and = binary "/usr/bin/gh" = host "api.github.com" = port 443 = layer "rest" = method "GET" = path "/repos/NVIDIA/OpenShell/issues/123" ; A raw L4 rule to the same host and port has no method or path to inspect. ; It covers L4 and anything that could ride over it, including REST. define-fun l4-candidate-allows Bool and = binary "/usr/bin/gh" = host "api.github.com" = port 443 or = layer "l4" = layer "rest" ; Check 1: does the broad candidate exceed the maximum? push assert and broad-candidate-allows not maximum-allows check-sat get-value layer method path pop ; Check 2: Does the narrow candidate GET, one issue exceed the maximum? push assert and narrow-candidate-allows not maximum-allows check-sat pop ; Check 3: Does the raw L4 rule to the same host and port exceed the maximum? push assert and l4-candidate-allows not maximum-allows check-sat get-value layer method path pop The first check returns sat, and the get-model above returns the witness below- a write to the root of the org that the safe maximal policy never permitted. sat ; check 1: broad candidate layer "rest" method "POST" path "/repos/NVIDIA/" unsat ; check 2: narrow candidate sat ; check 3: raw L4 layer "l4" method "" path "" The second check returns unsat. Every action the narrow candidate allows is already allowed inside the maximum. The third check is the OpenClaw story from earlier. The layer 4 candidate names the same host and port as is in our reference maximum policy, but over layer 4, which uses a wire protocol that cannot be enforced by OpenShell. The prover returns sat with layer = l4 and an empty method and path. In this case, we didn’t have to explicitly write a rule saying that L4 is broader than L7 REST, it effectively falls out of the encoding. How to encode the full OpenShell policy as formal logic OpenShell’s runtime prover models the following attributes for any network action: action = { binary: String, host: String, port: Int, layer: String, method: String, path: String } Note: the example action above is just a subset, the OpenShell runtime also covers filesystem, process, credential, and inference containment. We use code written in Rust to encode any policy changes proposed by agents into actions that can be checked by Z3. Once encoded, we can run a variety of checks. The first, a very general check- asks if the candidate proposed policy can do anything that the reference safe policy cannot do. js let candidate allows = policy allows candidate, &action ; let maximum allows = policy allows maximum, &action ; solver.assert Bool::and & candidate allows, maximum allows, ; match solver.check { SatResult::Unsat = MaximumPolicyCheck::WithinMax, SatResult::Sat = { let model = solver.get model .expect "sat result has a model" ; let counterexample = counterexample from model &model, &action .expect "model contains a symbolic action" ; MaximumPolicyCheck::ExceedsMax { counterexample } } SatResult::Unknown = MaximumPolicyCheck::Unsupported { reason: "Z3 returned unknown".to owned , }, } Conceptually: policy allows a = ⋁ rule allows rule, a rule allows rule, a = binary matches rule, a ∧ endpoint matches rule, a This is where you start to see some of the complexity of modeling an entire policy language. For example, OpenShell supports and glob semantics. These are compiled into Z3 regular expressions. As humans that are familiar with glob mechanics, we know that a single cannot cross / for paths or . for hosts- while can. So, we use our Rust code to encode this logic. Z3's regular-expression theory can then check for us whether the symbolic string belongs to the resulting language. That scope is deliberate: OpenShell models a regular-language fragment rather than arbitrary language-specific regular expressions with features such as backreferences, and unsupported policy surfaces fail closed. For a deep-dive on our research around containment, check out the OpenShell spike on maximum policies and narrowness budgets here: https://github.com/NVIDIA/OpenShell/blob/spike/maximal-policy-prover-subset/crates/openshell-prover/MAXIMUM POLICY ENVELOPE SPIKE.md https://github.com/NVIDIA/OpenShell/blob/spike/maximal-policy-prover-subset/crates/openshell-prover/MAXIMUM POLICY ENVELOPE SPIKE.md . Expert queries are just more formulas In the examples above, we have used a very general and extensible query, essentially asking if one proposed policy, however complex it is, is a subset of another safe policy that we have already reviewed. But, once we have the policy language modeled in Z3, we can ask about anything we want to. OpenShell’s policy advisor has four expert security checks built in, that run on any proposed policy and that are provided to the human or agent reviewer for approval. In adversarial testing, we have found that providing the results of these checks- which cannot be fooled, manipulated, or defeated directly, as context to an agent reviewer as an incredibly valuable way to increase the trustworthiness of agentic or human reviewers. Read more here: https://docs.nvidia.com/openshell/sandboxes/policy-advisor https://docs.nvidia.com/openshell/sandboxes/policy-advisor . Today, the OpenShell policy prover encodes the following expert queries which run on every proposed policy before approval. From the docs: | Category | Triggered when | |---|---| | link local reach | A rule reaches 169.254.0.0/16, fe80::/10, or a known metadata hostname. | | l7 bypass credentialed | A binary using a wire protocol the L7 proxy cannot inspect git-remote-https, ssh, nc gains reach to a host where a credential is in scope. | | credential reach expansion | A binary gains credentialed reach to a host, port it could not reach before. | | capability expansion | On a binary, host, port that already had credentialed reach, the proposal adds a new HTTP method. The finding cites the specific method. | Conclusion We’re incredibly excited about the promise of formal methods to help govern, audit, and build trustworthiness with agents over long horizon and continuously expanding and important tasks. If you’re working with formal methods, or interested in contributing to OpenShell- please reach out to us on the CNCF Slack, or join our weekly community meetings sign up at https://github.com/NVIDIA/OpenShell https://github.com/NVIDIA/OpenShell . Resources Definitive references for Z3, once the examples above start to feel familiar DeepMind’s verified code generation approach to the same problem- Blogs on AI review of agent permissions