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

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 to write a formal proof that a policy change proposed by an agent stays inside what you approved.

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: