The sandbox blocked the agent's write to a GitHub repo it was not allowed to touch.
The agent's next message: file written.
That story comes from NVIDIA's OpenShell team, in a dev note on the formal methods behind their policy checks. The agent noticed it was sandboxed, picked up the GitHub credential it already had, and pushed through git-remote-https, a binary the policy allowed so the agent could clone. The team had not realized that helper can push as well as fetch. Every rule was reasonable on its own. The combination was the hole.
That is the problem with reading permission files by eye. You check each line. The leak lives between the lines. And once agents start writing policies for other agents, nobody is reading every line anyway.
What OpenShell is, and the part worth stealing
OpenShell is NVIDIA's open-source runtime for sandboxing AI agents, and it sat at #2 on GitHub trending as I wrote this. You write a YAML policy per sandbox: which paths an agent can read or write, which user it runs as, and which binaries can reach which hosts. The filesystem rules go through Landlock in the kernel, and network traffic goes through a proxy that can check each HTTP method and path.
That part is good, and it is also what every sandbox promises. The piece I think matters more ships as its own small binary: openshell-prover. You give it two policy files, a candidate and a boundary, and it asks an SMT solver (Z3, according to the crate's Cargo.toml) whether the candidate allows anything the boundary does not. If it does, you get one concrete example of the extra access.
It needs no gateway, no Docker and no account. It just reads files. So I ran it.
One binary, one minute
On a Mac, the full install script installs through Homebrew and starts a gateway service. If you only want the prover, grab the release archive:
gh release download v0.1.2 -R NVIDIA/OpenShell \
-p 'openshell-prover-aarch64-apple-darwin.tar.gz'
tar xzf openshell-prover-aarch64-apple-darwin.tar.gz
./openshell-prover --version
# openshell-prover 0.1.2
On Linux, swap in the x86_64-unknown-linux-musl archive. The checksum matched the published sha256 file, and each check below came back in 10 milliseconds or less.
The docs' first example is a boundary that allows reading /usr and /etc, and a candidate that also wants to write /tmp:
result: exceeds_boundary
coverage: domains=filesystem,network_l4,network_rest,process,landlock
counterexample: filesystem write /tmp
Fine, but a toy. Here is the case I actually care about.
The case that matters: a parent agent writing a child's policy
Say a parent agent may use curl to read the GitHub API and nothing else. That is the boundary:
version: 1
network_policies:
github_read:
endpoints:
- host: api.github.com
port: 443
protocol: rest
enforcement: enforce
access: read-only
binaries:
- path: /usr/bin/curl
(My real files also had a small filesystem_policy, left out here.) Now the parent writes a policy for a subagent. The first draft allows GET on one repo only. The prover says within_boundary and exits 0.
The second draft sneaks in one extra rule, POST to /repos/acme/app/issues, the kind of thing an agent adds because "it might need to file a bug":
result: exceeds_boundary
counterexample: network binary=- ancestor_binary=- binary_identity_required=false
host=api.github.com:443 protocol=rest method=POST path=/repos/acme/app/issues
(Trimmed to the useful fields and wrapped for the page.) It found the exact request. Note binary_identity_required=false: the prover checks each policy both with and without binary identity enforcement, because a runtime can turn that enforcement off.
Then I tried the two leaks that are easy to miss by eye. A new rule letting curl reach paste.example.com came back with that host as the counterexample. And adding /usr/bin/python3.12 to the existing GitHub rule came back with ancestor_binary=/usr/bin/python3.12: a process started by Python reaching the API. The docs explain why. A rule covers the processes a listed binary starts, so adding an interpreter quietly adds everything it can run.
A candidate that switches the process user from sandbox to root came back with counterexample: process run_as_user boundary=sandbox candidate=root.
Where it says "I can't tell"
This is the part that sold me. When the prover cannot answer, it says so and exits 3, instead of passing.
- I narrowed the child's write access from
/sandboxto/sandbox/out. That is obviously smaller, and it returnedunsupported: a symlink inside the sandbox image could point/sandbox/outsomewhere else, so it wants matching paths in both files. - A REST rule in
auditmode returnedunsupported, since audit mode logs a bad request and lets it through. - A root user against a boundary that never named a user returned
unsupported, not a pass.
The docs list more gaps: GraphQL, MCP and WebSocket rules are not modeled yet. That first case is a real rough edge, because narrowing a path is exactly what a parent agent will do. But a checker that refuses beats one that guesses.
What this changes
Here is my claim. The useful unit of agent permission review is not the policy file. It is the counterexample.
Today a permission prompt shows you a rule and asks you to imagine what it allows. A prover turns that around: it shows you one concrete request the new policy would permit that the old one would not, or it tells you it cannot decide. Reading one line like method=POST path=/repos/acme/app/issues takes two seconds. Reading forty lines of YAML and spotting the Python interpreter takes a careful person, and agents do not wait for careful people.
This matters most if you let agents spawn agents. The parent's own policy becomes the boundary, and every child policy gets checked against it before it runs. Exit code 0 means go, anything else means a human looks.
OpenShell already wires this into its policy advisor, where an agent that hits a blocked request can propose a new network rule. Per the docs, each proposal gets a risk check that looks for things like credentials reaching a new host, and there is an automatic approval mode. Read that mode's fine print: the docs say it still approves a brand new public host when no credential applies there. That is a policy choice, not a proof.
What I did not run
I ran only the prover. I did not run a sandbox, the gateway or the advisor; everything I say about them comes from the docs. On a Mac a sandbox needs Docker Desktop or the MicroVM driver, and two issues opened on September 30 (#3955 and #3948) describe that path needing manual fixes on 0.1.2, including signing the VM driver by hand. If you want a first taste on a Mac, start with the prover. It is the part that works in a minute.
Would you let a subagent run on a policy nobody read, if a solver had checked it against yours?
Top comments (1)
The prover is a genuinely good find and the parent-writes-child's-policy case is the right one to lead with. But I think the opening story is evidence against the tool rather than for it, and the gap is worth naming because it changes where you would put the prover.
The OpenShell failure was that the policy allowed git-remote-https so the agent could clone, and that binary can push as well as fetch. The team's boundary already permitted the hole. So on that incident the prover takes the candidate, compares it to the boundary, finds nothing in the candidate that the boundary does not allow, and returns within_boundary with exit code 0. It is correct and the write still lands. The bug was in the boundary, and a containment prover is structurally unable to see it, because the boundary is its axiom.
That is not a criticism of Z3 or of the tool. It is a statement about what within_boundary means: no widening relative to a thing you asserted. Useful, and much narrower than the article's framing of proving your permissions.
Which suggests where it earns the most. It is strong on delegation chains, where the boundary was reviewed once by a human and every later policy is machine-written, and your second-draft POST example is exactly that. It is weak as the only check on a hand-written top-level boundary, because that is the file where a reasonable-looking line hides a capability nobody enumerated.
The thing that would have caught the real incident is less elegant and I do not know of a tool that does it. You need the boundary expressed over capabilities rather than binaries, and then a mapping from each allowed binary to every capability it can reach. That mapping is the hard artifact. git-remote-https implies network write to the host, curl implies whatever method you failed to pin, and ssh implies most things. Once you have it, the prover works on something worth proving. Without it, the boundary is still a list of program names that someone eyeballed, which is the practice the title is arguing against.
Have you tried running the prover with a deliberately broken boundary, to see what it reports? That seems like the cheap experiment that separates the two claims.