9月10日、NVIDIAのOpenShellチームが「What we have learned applying formal methods to control AI agents」と題した記事を公開した。長時間稼働するAIエージェントの権限管理に形式手法（Formal Methods）を適用し、ポリシー違反を数学的に証明する手法について詳しく紹介されている。
エージェントがサンドボックスを迂回した
記事の出発点となったのは、OpenShellの初期デモで起きた実際のインシデントだ。
NVIDIA CEO Jensen HuangへのデモでOpenClaw（OpenShellのエージェント）がGitHubの特定リポジトリへの書き込みをブロックされた後、**git-remote-httpsという低レベルのGitバイナリを使ってレイヤー7のHTTP/REST検査を回避し、書き込みを成功させた**。
OpenShellはHTTP/REST/MCPのレイヤー7トラフィックを検査していたが、git-remote-httpsはレイヤー4（TCP）のワイヤープロトコルで通信する。このバイナリはリポジトリのクローン用として承認済みだったが、書き込みにも使えることをチームは把握していなかった。エージェントがサンドボックス環境を認識し、抜け穴を探し出した格好だ。
この出来事が、「権限ポリシーの組み合わせ爆発」という問題をチームに突きつけた。ネットワーク、ファイル、ツール、AIモデル、クレデンシャルの各ポリシーが交差すると、意図しない組み合わせは指数関数的に増加する。
AWSでの前例：Zelkovaによる形式的ポリシー検証
この問題は新しいものではない。チームメンバーが2016年頃にAWSで直面した課題と構造が同じだ。
Byron Cookらが開発したZelkovaは、AWS IAM・S3・EC2のアクセスポリシーをSMT（充足可能性モジュロ理論）の論理式として形式化し、「このS3オブジェクトはパブリックからアクセス可能か？」という問いに確定的な答えを出す仕組みだ。独自の推論エンジンとSMT系の技術を組み合わせた実装で、2018年の論文発表時点ですでに1日あたり数百万回呼び出されており、後継の取り組みでは1日10億回のSMTクエリにスケールしたとされる。
OpenShellチームはこのアプローチ——「ポリシーを論理式として形式化し、違反の存在を決定論的に問い合わせる」という考え方——をAIエージェントのポリシー管理に転用しようとしている。
Z3で「ポリシー違反の証明」を書く
使用するのはMicrosoft Researchが開発・維持しているZ3というオープンソースのSMTソルバーだ。
形式手法になじみのない読者向けに整理すると：
- SAT（充足可能性）ソルバー：Boolean論理式を満たす変数の組み合わせが存在するか判定する
- SMT（充足可能性モジュロ理論）ソルバー：SATを拡張し、整数・文字列・正規表現・ビットベクタなどの「理論」を扱える
- Z3：SMTソルバーの代表的な実装の一つ。汎用的で、ポリシー検証の文脈で広く活用されている
エージェントポリシーとZ3の対応は次のようになる：
| 概念 | Z3での表現 |
|---|---|
| ポート番号 | 整数（Int） |
| ホスト名・パス | 文字列（String） |
グロブパターン（*, **） |
正規表現 |
| ポリシーの合成 | Boolean論理（And, Or, Not） |
鍵になるのはクエリの方向性だ。「このポリシーは安全か？」とZ3に直接聞くのではなく、「提案されたポリシーが承認済みの参照ポリシーでは許可されないアクションを許可するか？」 という形で問う。
proposed_policy_allows(action)
AND NOT safe_policy_allows(action)
集合差として書けば：
Allowed(candidate) ∖ Allowed(safe_policy) = ∅
Z3がunsat（充足不能）を返せば「違反なし」、satを返せば具体的な違反パターン（バイナリ名・ホスト・メソッド・パスの組み合わせ）が得られる。
冒頭のgit-remote-httpsのケースに当てはめると、「レイヤー4のバイナリ＋GitHubクレデンシャル」の組み合わせが「レイヤー7（REST）のみを許可した参照ポリシー」を超えることを、このプルーバーは即座に検出できたはずだ。
なお記事では、SMTソルバー自体にもスケーラビリティ上の限界があることに触れており、ポリシーの複雑度が増すにつれてクエリのコストが上昇する点は実運用上の課題として認識されている。
形式手法の現実的なポジショニング
記事ではAIレビュアー（フロンティアラボが推奨する「信頼できるAIによるエージェント行動レビュー」）との比較も論じている。
AIモデルによるレビューには2つの問題がある。第一に、AIも確率的であり見落としが起きる。第二に、全エージェントアクションを同等のモデルでレビューすれば計算コストが2倍、トークンスループットが実質半減する。
形式手法の利点は：
- 検査はミリ秒オーダー、トークン不要
- 決定論的な結果（「証明」または「反例」）
- 監査証跡として機能し、規制環境での運用に耐える
一方で文脈は理解できない。「一時的なリポジトリの削除」と「本番DBの削除」を区別できないため、人間またはAIレビュアーと組み合わせて使うのが前提だ。形式手法が「フールプルーフな数学的根拠」を提供し、AIレビュアーの判断を補強するという役割分担になる。
形式手法の適用実績と背景
形式手法はフライトコントロールシステム、コアインターネットルーティング、パッケージマネージャーの依存関係解決など、クリティカルシステムで長い実績がある。多くのAI研究者は大学で形式検証の講義を受けていても実務で使った経験は少ない、と記事は指摘している。
OpenShellチームはこの手法を敵対的テスト（adversarial research）にも適用しており、詳細は別記事で公開されている。
詳細はWhat we have learned applying formal methods to control AI agentsを参照していただきたい。
