Hanzo ya publicó las pruebas formales de su infraestructura de agentes de IA

Hoy dejamos en código abierto pruebas formales chequeadas por máquina para la pila de infraestructura de Hanzo AI. No son pruebas de software ni auditorías: son garantías matemáticas que verifica el chequeador de tipos de Lean 4.

Qué quedó demostrado

Seguridad de los agentes (6 pruebas)

• Límites de capacidad: un agente no puede pasar los permisos que se le otorgaron
• Prevención de la escalada: ninguna secuencia de acciones llega 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 reduce, 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 calificación de calidad ante fallas bizantinas
• Cómputo confidencial: aislamiento del enclave y frescura de la atestación
• Coordinación del enjambre: reparto justo de tareas y convergencia del balanceo de carga
• Corrección de la facturación: el uso medido nunca cobra de más

Puerta de enlace y plataforma (6 pruebas)

• Validación de tokens, equidad del límite de tasa y corrección de la ventana deslizante
• Seguridad del rollback 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 llaves maestras nunca cruzan el límite del HSM

En números

• 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, fijos 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. «Por lo general funciona» no alcanza 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 de 2014 a 2026
• Sitio: proofs.hanzo.network

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