Hanzo 發表 AI 代理基礎架構的形式化證明

今天我們開源 Hanzo AI 基礎架構堆疊的機器檢驗形式化證明。它們不是測試，也不是稽核。它們是由 Lean 4 型別檢查器核對的數學保證。

已經證明的內容

代理安全（6 項證明）

• 能力邊界：代理不能超出被授予的權限
• 防止提權：沒有任何動作序列通向未授權的能力
• MCP 工具呼叫：內容視窗在多次呼叫之間保持
• 委派的單調性：被委派的權限只會收窄，不會擴大
• 工作流程順序：DAG 執行遵守相依邊
• 記憶隔離：代理的回憶只追加，並受關聯性約束

計算層（4 項證明）

• Proof of AI 共識：TEE 證明鏈的完整性，以及拜占庭故障下品質評分的收斂
• 機密計算：飛地隔離與證明的新鮮度
• 叢集協調：工作分配的公平性與負載平衡的收斂
• 計費正確：計量用量從不多收費

閘道與平台（6 項證明）

• 權杖校驗、速率限制的公平性，以及滑動視窗的正確性
• blue-green 部署回滾的安全性，以及零停機不變量
• SBOM 供應鏈的完整性，以及弱點追蹤的單調性

KMS（1 項證明）

• 秘密存取清單的強制執行：主金鑰從不越過 HSM 邊界

數字

• 17 個 Lean 4 檔案，0 個 sorry，0 個建置錯誤
• 3 條公理，都在刻畫硬體邊界（TEE 隔離、HSM 周界、外部驗證）
• Lean 4.14.0 + Mathlib 4.14.0，已固定，可重現
• Apache 2.0 授權

為什麼 AI 代理需要形式化驗證

代理正在獲得自主性。它們使用工具、管理資金、做出決定。當代理拿著你的 API 金鑰、資料庫和客戶時，「通常能跑」是不夠的。

形式化驗證證明 任何可能的執行 都不會破壞安全性質。不是「我們測了 10,000 個例子」。是全部。代理不能提升權限，這個證明不是機率。它是數學。

連結

• 證明：github.com/hanzoai/proofs
• 論文：github.com/hanzoai/papers — 2014 年至 2026 年的 34 篇研究論文
• 站點：proofs.hanzo.network

形式化驗證工作涵蓋整個 Hanzo 生態，從 AI 閘道到代理基礎架構。另見 hanzoai/proofs。