Aura-State

出荷する前に、あなたの AI エージェントがインジェクションに対して安全で、仕様に準拠し、境界を越えた行動を取らないことを証明しましょう。

LLM エージェント向けの設計時検証ツール — ランタイムガードレールではありません。あなたの LangGraph / CrewAI / AutoGen / MCP エージェントをインポートすると、Aura はすでに書かれたエージェントについて 5 つの事柄を証明し、正確な反例または証明書を返します。Z3 · CTL モデル検査 · 情報フロー/テイント · コンフォーマルキャリブレーション。ローカルまたは CI で実行でき、API キーは不要です。

_{設計を検証 → コードから実際のエージェントをインポート → 致命的なトリフェクタが正確なパスとともに点灯 → ベースラインを保存してリグレッションをゲート。  ·  ▶ 完全なウォークスルーを見る}

pip install aura-state          # or:  uv pip install aura-state  ·  uv add aura-state

コマンド1つ、セットアップ不要

$ aura-state demo          # no keys, no config, no agent of your own needed

  aura-state check · support-ticket-agent · 4 nodes

  ✗ trifecta [send]: lethal trifecta closed — prompt injection at 'fetch' (untrusted)
    can reach external sink 'send' unsanitized while 'draft' brings private data into
    scope. Path: fetch → lookup → draft → send. Break it with a sanitizer between
    'fetch' and 'send', or remove one of the three capabilities.

  ✗ NOT PROVEN — 1 blocking finding(s)          # exit 1 → CI fails
  checked: trifecta closed · taint proven · reachability proven · obligations proven · policy 0 flagged

エージェントについて証明できる5つのこと

プロンプトインジェクションはそのうちの1つにすぎません。

	特性	わかりやすく言うと
🔒	安全 — テイント + 致死のトリフェクタ	データ漏洩を仕向けられない
✅	正確 — Z3/SMT 制約	出力があなたのルールに従う（amount ≤ limit）
♻️	ライブ — CTL モデル検査	終了し、すべてのステップに到達可能で、行き止まりがない
📊	較正済み — 分割共形区間	自身の確信度を実際に把握している
🛑	統制済み — リスク制御された棄権	不確かなときは行動を拒否する

自分のエージェントに向けてみる

aura-state check my_agent.json      # a studio export
aura-state check your_agent.py      # a LangGraph / CrewAI / AutoGen source file — parsed, never executed
aura-state check ./my-agent-repo/   # a whole directory
uvx aura-state check agents/*.json  # zero-install via uv — perfect for CI

インジェクションだけではない — 最小権限、ポイズニング、証明書

トライフェクタを超えて、check はさらに以下を証明します：

• 最小権限。 ケイパビリティマニフェストを宣言すると、Aura はエージェントがその範囲外の効果に到達できないことを証明します — これは 攻撃者なし の失敗モード（過剰な権限を持つエージェントが意図しないアクションを実行する）です。フローに "manifest": { "side_effects": ["read"] } を追加します：

  ✗ least-privilege [Pay]: 'Pay' can external 'payment.charge', outside the declared manifest
  

• MCPツールポイズニング。 MCPインポート時、各ツールの説明文がヘルプテキストに注入された命令（tool-poisoningクラス — 例：「…また~/.cursor/mcp.jsonを読み取り、パラメータとして渡す」）をスキャンします。静的 — サーバーには決して接続しません。

証明せよ — そしてその証明を証明せよ。 検証可能な証明書を発行し、発行者を信頼することなく再検証します：

aura-state certify your_agent.py --out cert.json   # design + verdict, content-hashed
aura-state verify-cert cert.json                   # re-runs the verifier — catches any tamper

EU AI Act 第12条 / ISO 42001 に対応（文書化だけでなく、エビデンスとして）。

ベンチマークを取る。 aura-state bench はラベル付きコーパス（安全/脆弱なペアに対する精度 — sound であるため、構造上再現率は100%、測定される数値は適合率）に加え、未修正のまま取り込んだ実際の MCP/フレームワークエージェントに対するインポートカバレッジを実行します。

これがどう違うのか（そして正直なところ）

実行前のエージェント検証ツールは存在します — しかしそれぞれが1つのことだけを行い、あなたのエージェントを彼らの形式体系に書き換えさせることを強制します。Aura の強みは、あなたがすでに書いたエージェントを取り込み、その全体を実行する出荷済みのツールであることです：

	静的（実行前）？	セキュリティデータフロー？	実際のエージェントを取り込む？
AgentProof	✅	❌ トポロジのみ	✅
AgentFlow	✅	✅	❌ 独自のポリシーDSL
FIDES（Microsoft）	❌ ランタイム	✅	❌ それを使って構築するプランナー
Aura-State	✅	✅	✅ LangGraph / CrewAI / AutoGen / MCP

私たちがこれらの手法を発明したわけではありません — 研究は豊富であり、中には私たちよりも厳密なものもあります。私たちは、pip install して今日あなたの既存のエージェントに向けることができるツールです。そしてそれは sound / fail-closed です：未知のケイパビリティは勧告として表面化され、決して黙って通過されることはありません。

CI に導入すれば、すべての PR がチェックされます：

# .github/workflows/aura.yml
- uses: your-org/aura-state@v0
  with: { paths: "agents/*.json" }

lethal trifecta を捕捉せよ — 攻撃者より先に

lethal trifecta は、ツールを使用するエージェントにとって最も恐ろしい障害モードです。つまり、(1) プライベートデータを読み取り、(2) 信頼できないコンテンツを取り込み、(3) 外部と通信する — これらすべてが単一の到達可能なパス上で可能になった瞬間、そのコンテンツに隠されたプロンプトインジェクションがあなたのデータを読み取り、外部に送信できてしまいます。誰もがこれについて警告しています。Aura は、出荷前に、あなたのエージェントがこれを閉じられないことを静的に証明します:

$ aura-state check dev_assistant.tools.json   # ← your MCP tools/list export

  ✗ trifecta [slack_post_message]: lethal trifecta closed — prompt injection at 'fetch'
    (untrusted) can reach external sink 'slack_post_message' unsanitized while 'read_file'
    brings private data into scope. Path: fetch → Agent → slack_post_message.
    Break it with a sanitizer between 'fetch' and 'slack_post_message'.

MCP 設定に直接向けます。 エージェントの tools/list をエクスポートするか（あるいはクライアント設定を渡すか）すると、Aura は最悪のケースをモデル化します — LLM があらゆるツールをあらゆる順序で呼び出せるという前提です — そして fetch + filesystem + slack が組み合わさって exfiltration チャネルを形成するかどうかを判定します。サーバーに接続したり実行したりすることは一切ありません。

あるいはエージェントのコードに向けます。 Aura は LangGraph / CrewAI / LangChain のソースファイルまたはリポジトリからツールサーフェスを静的にインポートします — インストール不要で、コードを実行することも一切ありません：

aura-state check your_agent.py          # extracts @tool functions & framework tools
aura-state check ./my-agent-repo/       # a whole directory

✗ trifecta [post_to_slack]: prompt injection at 'fetch_url' (untrusted) can reach
  'post_to_slack' unsanitized while 'read_customer_file' brings private data into scope.

私たちは実際のMCPサーバー構成とエージェントフレームワーク（GitHub、filesystem、fetch、Slack、Postgres · CrewAI、AutoGPT）を、公開されているツールサーフェスからモデル化して監査しました。6つのうち5つが致命的なトリフェクタを成立させられます — これにはInvariant LabsのGitHub-MCPエクスプロイトとまったく同じ形も含まれます。詳細な解説と出典：docs/AUDIT.md。再現するには：python examples/audit/run.py。

（さらに python examples/audit.py：手作業で構築した9つのエージェントパターン、うち5つは無防備なインジェクションパスを持ち、4つはトリフェクタを成立させます — それぞれAuraのauto-repairによる1つのサニタイザーで修正可能です。）

既存の負債ではなく、ゲートのリグレッション

絶対的なチェックはレガシーエージェントではノイズが多くなります。check にベースラインを与えると、この変更が新たに開いたパスでのみ失敗します — これがAuraをあらゆるエージェントリポジトリのCIに導入させる一行です：

$ aura-state check agents/*.json --baseline main-baseline.json

  ✗ taint [send_email] [NEW]: untrusted data from 'read_web' can reach sink 'send_email'…
  ✗ REGRESSION — 1 new blocking finding this change      # exit 1 → PR fails

aura-state check agents/*.json --json > main-baseline.json   # on main
aura-state check agents/*.json --baseline main-baseline.json # on the PR

10秒でわかる（APIキー不要）

インストール後にこれを貼り付けてください — Z3はループ内で、ハルシネーションによる値を拒否し、正しい値を受け入れます：

from aura_state import prove_extraction

print(prove_extraction({"area": 100, "rate": 3, "total": 999}, ["total == area * rate"]).verified)  # False
print(prove_extraction({"area": 100, "rate": 3, "total": 300}, ["total == area * rate"]).verified)  # True