Hanzo Ships Formal Proofs for AI Agent Infrastructure
Machine-checked Lean 4 proofs for agent safety, MCP protocol, PoAI consensus, and platform operations
Today we open-sourced machine-checked formal proofs for the Hanzo AI infrastructure stack. These aren't tests or audits — they're mathematical guarantees verified by Lean 4's type checker.
What's Proven
Agent Safety (6 proofs)
- Capability bounds: agents cannot exceed granted permissions
- Escalation prevention: no action sequence leads to unauthorized capability
- MCP tool invocation: context window preservation across tool calls
- Delegation monotonicity: delegated authority only narrows, never widens
- Workflow ordering: DAG execution respects dependency edges
- Memory isolation: agent recall is append-only and relevance-bounded
Compute Layer (4 proofs)
- Proof of AI consensus: TEE attestation chain integrity, quality scoring convergence under Byzantine faults
- Confidential compute: enclave isolation, attestation freshness
- Swarm coordination: task distribution fairness, load balancing convergence
- Billing correctness: metered usage never overcharges
Gateway & Platform (6 proofs)
- Token validation, rate limit fairness, sliding window correctness
- Blue-green deploy rollback safety, zero-downtime invariant
- SBOM supply chain completeness, vulnerability tracking monotonicity
KMS (1 proof)
- Secret access-list enforcement, master keys never cross HSM boundary
By the Numbers
- 17 Lean 4 files, 0 sorry, 0 build errors
- 3 axioms — all modeling hardware boundaries (TEE isolation, HSM perimeter, external auth)
- Lean 4.14.0 + Mathlib 4.14.0 — pinned, reproducible
- Apache 2.0 licensed
Why Formal Verification for AI Agents
Agents are gaining autonomy. They use tools, manage money, make decisions. "It usually works" isn't good enough when an agent has access to your API keys, your database, and your customers.
Formal verification proves that no possible execution violates the safety properties. Not "we tested 10,000 cases." All of them. The proof that an agent cannot escalate privileges isn't probabilistic — it's mathematical.
Links
- Proofs: github.com/hanzoai/proofs
- Papers: github.com/hanzoai/papers — 34 research papers spanning 2014-2026
- Site: proofs.hanzo.network
The formal verification work covers the full Hanzo ecosystem, from the AI gateway to agent infrastructure. See also hanzoai/proofs.
Read more
Hanzo Brain: Local-First Knowledge Graph for Agents
A single SQLite file your agent reads from every runtime. Zero LLM round-trips for graph ops, FTS5 plus vector plus typed-edge extraction at write time.
The Complete AI Agent Stack: Models, Compute, and Tools in One Platform
Hanzo AI introduces the first platform combining 100+ AI models, cloud compute, GPU access, and 260+ MCP tools under a single developer account.
MCP: 260 Tools for AI Models
How we built 260+ tools using Model Context Protocol, enabling AI models to interact with the world.