Hanzo publica pruebas formales para la infraestructura de agentes de IA

Hoy publicamos en código abierto pruebas formales verificadas por máquina para la pila de infraestructura de Hanzo AI. No son tests ni auditorías: son garantías matemáticas que comprueba el verificador de tipos de Lean 4.

Qué está demostrado

Seguridad de los agentes (6 pruebas)

• Límites de capacidad: un agente no puede superar los permisos concedidos
• Prevención de la escalada: ninguna secuencia de acciones lleva a una capacidad no autorizada
• Invocación de herramientas MCP: la ventana de contexto se conserva entre llamadas
• Monotonía de la delegación: la autoridad delegada solo se estrecha, nunca se amplía
• Orden del flujo de trabajo: la ejecución del DAG respeta las aristas de dependencia
• Aislamiento de la memoria: el recuerdo del agente es solo de adición y está acotado por la relevancia

Capa de cómputo (4 pruebas)

• Consenso Proof of AI: integridad de la cadena de atestación TEE y convergencia de la puntuación de calidad ante fallos bizantinos
• Cómputo confidencial: aislamiento del enclave y frescura de la atestación
• Coordinación del enjambre: reparto justo de tareas y convergencia del equilibrado de carga
• Corrección de la facturación: el uso medido nunca cobra de más

Pasarela y plataforma (6 pruebas)

• Validación de tokens, equidad del límite de tasa y corrección de la ventana deslizante
• Seguridad de la reversión en un despliegue blue-green e invariante de cero tiempo de inactividad
• Integridad de la cadena de suministro del SBOM y monotonía del seguimiento de vulnerabilidades

KMS (1 prueba)

• Cumplimiento de la lista de acceso a secretos: las claves maestras nunca cruzan el límite del HSM

En cifras

• 17 archivos de Lean 4, 0 sorry, 0 errores de compilación
• 3 axiomas, todos modelan límites de hardware (aislamiento TEE, perímetro del HSM, autenticación externa)
• Lean 4.14.0 + Mathlib 4.14.0, fijados y reproducibles
• Licencia Apache 2.0

Por qué la verificación formal para agentes de IA

Los agentes ganan autonomía. Usan herramientas, manejan dinero y toman decisiones. «Suele funcionar» no basta cuando un agente tiene acceso a tus claves de API, a tu base de datos y a tus clientes.

La verificación formal demuestra que ninguna ejecución posible viola las propiedades de seguridad. No es «probamos 10.000 casos». Son todos. La prueba de que un agente no puede escalar privilegios no es probabilística: es matemática.

Enlaces

• Pruebas: github.com/hanzoai/proofs
• Artículos: github.com/hanzoai/papers — 34 artículos de investigación entre 2014 y 2026
• Sitio: proofs.hanzo.network

El trabajo de verificación formal cubre todo el ecosistema Hanzo, desde la pasarela de IA hasta la infraestructura de agentes. Véase también hanzoai/proofs.