Hanzo が AI エージェント基盤の形式証明を公開

本日、Hanzo AI のインフラストラクチャ・スタックについて、機械が検査した形式証明をオープンソースにします。テストでも監査でもありません。Lean 4 の型検査器が確かめる数学的な保証です。

証明されていること

エージェントの安全性（6 件）

• 能力の上限: エージェントは与えられた権限を超えられない
• 昇格の防止: どの行動列も、許されていない能力には至らない
• MCP ツール呼び出し: コンテキストウィンドウは呼び出しをまたいで保たれる
• 委任の単調性: 委任された権限は狭まるだけで、広がることはない
• ワークフローの順序: DAG の実行は依存辺を守る
• 記憶の隔離: エージェントの想起は追記のみで、関連性によって限られる

計算層（4 件）

• Proof of AI コンセンサス: TEE 証明鎖の完全性と、ビザンチン障害のもとでの品質スコアの収束
• 機密計算: エンクレーブの隔離と証明の鮮度
• スウォーム調整: タスク配分の公平さと負荷分散の収束
• 課金の正しさ: 計測された利用が過大に請求されることはない

ゲートウェイとプラットフォーム（6 件）

• トークン検証、レート制限の公平さ、スライディングウィンドウの正しさ
• blue-green デプロイのロールバック安全性と、無停止の不変条件
• SBOM サプライチェーンの完全性と、脆弱性追跡の単調性

KMS（1 件）

• 秘密のアクセスリストの強制: マスター鍵は HSM の境界を越えない

数字で見る

• Lean 4 のファイル 17 本、sorry は 0、ビルドエラーは 0
• 公理 3 つ。いずれもハードウェアの境界を表す（TEE の隔離、HSM の周縁、外部認証）
• Lean 4.14.0 + Mathlib 4.14.0。ピン留めされ、再現できる
• ライセンスは Apache 2.0

AI エージェントに形式検証が要る理由

エージェントは自律を増しています。ツールを使い、お金を扱い、判断します。エージェントが API キーとデータベースと顧客に触れるとき、「だいたい動く」では足りません。

形式検証は、起こりうるどの実行も安全性質を破らないことを証明します。「1 万件試した」ではありません。すべてです。エージェントが権限を昇格できないという証明は確率ではありません。数学です。

リンク

• 証明: github.com/hanzoai/proofs
• 論文: github.com/hanzoai/papers — 2014 年から 2026 年にわたる研究論文 34 本
• サイト: proofs.hanzo.network

形式検証の仕事は、AI ゲートウェイからエージェント基盤まで、Hanzo の生態系全体を覆います。あわせて hanzoai/proofs を見てください。