A Hanzo publica provas formais para a infraestrutura de agentes de IA

Hoje publicamos em código aberto provas formais verificadas por máquina para a pilha de infraestrutura da Hanzo AI. Não são testes nem auditorias: são garantias matemáticas conferidas pelo verificador de tipos do Lean 4.

O que está provado

Segurança dos agentes (6 provas)

• Limites de capacidade: um agente não pode ultrapassar as permissões concedidas
• Prevenção de escalada: nenhuma sequência de ações leva a uma capacidade não autorizada
• Invocação de ferramentas MCP: a janela de contexto se preserva entre chamadas
• Monotonia da delegação: a autoridade delegada só se estreita, nunca se amplia
• Ordem do fluxo de trabalho: a execução do DAG respeita as arestas de dependência
• Isolamento de memória: a memória do agente é somente de acréscimo e limitada pela relevância

Camada de computação (4 provas)

• Consenso Proof of AI: integridade da cadeia de atestação TEE e convergência da pontuação de qualidade diante de falhas bizantinas
• Computação confidencial: isolamento do enclave e frescor da atestação
• Coordenação do enxame: distribuição justa de tarefas e convergência do balanceamento de carga
• Correção da cobrança: o uso medido nunca cobra a mais

Gateway e plataforma (6 provas)

• Validação de tokens, equidade do limite de taxa e correção da janela deslizante
• Segurança do rollback de um deploy blue-green e invariante de zero tempo de inatividade
• Completude da cadeia de suprimentos da SBOM e monotonia do rastreamento de vulnerabilidades

KMS (1 prova)

• Aplicação da lista de acesso a segredos: as chaves mestras nunca cruzam a fronteira do HSM

Em números

• 17 arquivos Lean 4, 0 sorry, 0 erros de build
• 3 axiomas, todos modelam fronteiras de hardware (isolamento TEE, perímetro do HSM, autenticação externa)
• Lean 4.14.0 + Mathlib 4.14.0, fixados e reproduzíveis
• Licença Apache 2.0

Por que verificação formal para agentes de IA

Os agentes ganham autonomia. Usam ferramentas, lidam com dinheiro e tomam decisões. «Em geral funciona» não basta quando um agente tem acesso às suas chaves de API, ao seu banco de dados e aos seus clientes.

A verificação formal prova que nenhuma execução possível viola as propriedades de segurança. Não é «testamos 10.000 casos». São todos. A prova de que um agente não pode escalar privilégios não é probabilística: é matemática.

Links

• Provas: github.com/hanzoai/proofs
• Artigos: github.com/hanzoai/papers — 34 artigos de pesquisa de 2014 a 2026
• Site: proofs.hanzo.network

O trabalho de verificação formal cobre todo o ecossistema Hanzo, do gateway de IA à infraestrutura de agentes. Veja também hanzoai/proofs.