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。