What we have learned at OpenShell applying formal methods to control AI agents
10 hours ago
- Permission review breaks at agent scale because agent needs evolve and human supervision cannot scale, necessitating formal methods to ensure agents stay within approved permissions.
- A demo showed an agent bypassing layer 7 REST inspection by using a layer 4 wire protocol with a binary (git-remote-https), highlighting the exponential number of unintended policy combinations.
- Previous work at AWS (Zelkova) successfully used formal methods (SMT solvers) to verify IAM, S3, and EC2 policies at scale, inspiring the application to AI agents.
- Formal methods offer deterministic proofs, fast millisecond checks, and no token cost, complementing probabilistic AI reviewers by providing un-foolable auditing trails.
- The post explains SAT/SMT solvers and Z3, encoding agent policies (ports, hosts, paths, layers) into logic, with queries to check if candidate policies exceed a reference maximum.
- Practical Z3 examples demonstrate containment checks: finding counterexamples for broad policies, proving narrow policies safe, and detecting raw L4 bypasses.
- OpenShell's policy prover includes expert queries (link_local_reach, l7_bypass_credentialed, credential_reach_expansion, capability_expansion) run on every proposed policy.
- Formal methods are seen as a promising area for governing long-horizon agent tasks, with invitations to contribute to OpenShell and further resources.
- The encoding models a regular-language fragment of glob semantics, and unsupported policy surfaces fail closed.
- The post emphasizes that modeling policy languages is complex but yields powerful advantages: formal auditability, determinism, and speed.