8月19日、Common Expression Language Teamが「Securing the agentic era: Introducing formal verification for CEL」と題した記事を公開した。AIエージェントが自律的にポリシーを生成する時代に対応するため、CELの形式検証フレームワークをオープンソースとして公開したことについて詳しく紹介されている。

偽陽性ゼロ・100%再現可能な実バグのみを報告する設計

このフレームワークが単なる静的解析ツールと一線を画す最大の特徴は、「Violated」として報告された問題は100%再現可能な実バグであることが保証されるという設計にある。

形式検証ツールの実用上の課題として、ソルバーが理解できないカスタム関数や外部変数に遭遇したときに偽のバグを報告してしまう「ソルバーハルシネーション」がある。このフレームワークはこれを「3パスの汚染追跡（taint tracking）」で回避する。マッピングされていないカスタム関数が関与する潜在的問題はViolatedではなくInconclusiveとして分類され、CIパイプラインが誤検知で止まることを防ぐ。

また、SMT量化子内での無限ループを防ぐバウンデッドモデルチェッキング（検証の深さを設定可能）も備える。[[1], [2]] == [[1], [2]]のようなネストした構造の等価検証で検証コストが爆発しないよう制御できる。

AIが書いたポリシーを、数学的に証明する

LLMベースのAIエージェントがコードやポリシーを自動生成する動きが急速に広がっている。しかしユニットテストは「無限に存在しうる入力の組み合わせ」を網羅できない。テストに過適合したポリシーが本番環境で予期せぬ挙動を起こすリスクは現実のものだ。

GoogleのCommon Expression Language（CEL）チームはこの問題に対し、ヒューリスティックなテストを超えた解法——数学的証明——を提供するCEL Formal Verification Frameworkを公開した。

形式検証（Formal Verification）とは、プログラムやシステムの性質を数学的な論理式として記述し、「あらゆる入力に対して成立するか」を機械的に証明する手法だ。テストが「サンプルとなる有限の入力で動作を確認する」のに対し、形式検証は入力空間全体を対象とする。内部では、Microsoftが開発した定理証明器（SMTソルバー）**Z3**を使用する。SMTソルバーとは、論理式・算術・配列などを含む制約充足問題を自動的に解くソフトウェアで、形式検証・バグ発見・セキュリティ解析などの分野で広く用いられている。

CELはKubernetesのAdmission PolicyやGoogle Cloud IAMなど、インフラのポリシー記述に広く使われている式言語だ。このフレームワークはCEL式が「すべての入力に対して正しく動作するか」を数学的に検証する。

形式検証が答えを出せる問いの例として、記事では以下を挙げている。

• 「未承認のリクエストが本番環境に通り抜けるような入力の組み合わせは存在するか？」
• 「AIがリファクタリングしたポリシーは、元のポリシーと完全に同じ挙動をするか？」
• 「悪意ある操作で評価エラーを意図的に引き起こせるか？」

3つの検証パターン

1. 等価チェック（Equivalence）——演算子優先度のバグを即座に検出

AIエージェントがポリシーをリファクタリングする際に起きやすい「意味を変えてしまうバグ」の典型例が提示されている。ポート80または443を許可するルールをリファクタリングした結果：

equiv
  (is_prod && port == 80) || (is_prod && port == 443)
  <=>
  is_prod && port == 80 || port == 443

論理ANDはORより演算子優先度が高いため、右辺は(is_prod && port == 80) || port == 443と解釈される。つまり非本番環境でもポート443が通過してしまう。フレームワークは即座にViolatedを返し、is_prod = falseかつport = 443というカウンター例を出力する。

2. 妥当性チェック（Validity）——整数空間を網羅的に探索

あるバリデーションルールが「すべての入力に対して成立するか」を検証する。「ポートは80以下か1024超のはず」という前提で書かれた式に対して：

valid request.port > 1024 || request.port <= 80

フレームワークは整数空間全体を探索し、request.port = 81というカウンター例を出力してViolatedと判定する。人間がテストケースを書く場合に見落としやすい「境界の隙間」を機械的に発見できる。

3. CELポリシー形式での不変条件チェック（Invariants）

複数のルールや変数が絡む複雑なポリシーには、CEL policy形式のassume/assertブロックを使う。「承認なし、かつ管理者でなければ、結果はfalseになるはず」という不変条件を定義すると：

verification:
  invariants:
    - id: universal_no_unapproved_privileged_prod
      assume:
        - 'request.has_approval == false'
        - 'variables.is_admin == false'
      assert:
        - 'rule.result == false'

上記のポリシーにはrequest.is_privileged && request.is_prodを承認チェックなしに通過させる条件が紛れ込んでいる。フレームワークはこれを検出し、具体的な悪用入力例を出力する。この検証をCI/CDパイプラインに組み込むことで、AIが生成したポリシー変更を自動的にゲートできる。

入手と利用

GitHubリポジトリから利用可能で、対話的に試せるREPLツールも提供されている。イシューやプルリクエスト、フィードバックは歓迎とのことだ。

詳細はSecuring the agentic era: Introducing formal verification for CELを参照していただきたい。