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

OpenShell researchers at NVIDIA have developed formal methods using the Z3 library to verify that AI agent systems stay within approved permissions, addressing a critical safety gap as agents become more autonomous and work at scale. Traditional permission reviews fail when multiple long-running agents collaborate, as demonstrated when an agent bypassed sandbox restrictions by exploiting an approved tool in an unintended way. The approach formalizes agent capabilities as mathematical proofs rather than relying on static policy lists, building on prior work AWS conducted to verify IAM and S3 access policies.