Stop eyeballing your agent's permissions. Prove them.

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 /sandbox to /sandbox/out. That is obviously smaller, and it returned unsupported: a symlink inside the sandbox image could point /sandbox/out somewhere else, so it wants matching paths in both files.
• A REST rule in audit mode returned unsupported, 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?