Hanzo publie des preuves formelles pour l'infrastructure des agents d'IA

Nous publions aujourd'hui en open source des preuves formelles vérifiées par machine pour la pile d'infrastructure de Hanzo AI. Ce ne sont ni des tests ni des audits : ce sont des garanties mathématiques contrôlées par le vérificateur de types de Lean 4.

Ce qui est prouvé

Sûreté des agents (6 preuves)

• Bornes de capacité : un agent ne peut pas dépasser les permissions accordées
• Prévention de l'escalade : aucune suite d'actions ne mène à une capacité non autorisée
• Invocation d'outils MCP : la fenêtre de contexte est préservée d'un appel à l'autre
• Monotonie de la délégation : l'autorité déléguée ne fait que se restreindre, jamais s'élargir
• Ordre du flux de travail : l'exécution du DAG respecte les arêtes de dépendance
• Isolement de la mémoire : le rappel de l'agent est en ajout seul et borné par la pertinence

Couche de calcul (4 preuves)

• Consensus Proof of AI : intégrité de la chaîne d'attestation TEE et convergence du score de qualité face à des fautes byzantines
• Calcul confidentiel : isolement de l'enclave et fraîcheur de l'attestation
• Coordination de l'essaim : équité de la répartition des tâches et convergence de l'équilibrage de charge
• Exactitude de la facturation : l'usage mesuré ne surfacture jamais

Passerelle et plateforme (6 preuves)

• Validation des jetons, équité de la limite de débit et exactitude de la fenêtre glissante
• Sûreté du retour arrière d'un déploiement blue-green et invariant de zéro interruption
• Complétude de la chaîne d'approvisionnement du SBOM et monotonie du suivi des vulnérabilités

KMS (1 preuve)

• Application de la liste d'accès aux secrets : les clés maîtresses ne franchissent jamais la frontière du HSM

Les chiffres

• 17 fichiers Lean 4, 0 sorry, 0 erreur de compilation
• 3 axiomes, qui modélisent tous des frontières matérielles (isolement TEE, périmètre du HSM, authentification externe)
• Lean 4.14.0 + Mathlib 4.14.0, épinglés et reproductibles
• Licence Apache 2.0

Pourquoi la vérification formelle pour les agents d'IA

Les agents gagnent en autonomie. Ils utilisent des outils, gèrent de l'argent, prennent des décisions. « Ça marche en général » ne suffit plus lorsqu'un agent a accès à vos clés d'API, à votre base de données et à vos clients.

La vérification formelle prouve qu'aucune exécution possible ne viole les propriétés de sûreté. Pas « nous avons testé 10 000 cas ». Tous. La preuve qu'un agent ne peut pas élever ses privilèges n'est pas probabiliste : elle est mathématique.

Liens

• Preuves : github.com/hanzoai/proofs
• Articles : github.com/hanzoai/papers — 34 articles de recherche de 2014 à 2026
• Site : proofs.hanzo.network

Le travail de vérification formelle couvre tout l'écosystème Hanzo, de la passerelle d'IA à l'infrastructure d'agents. Voir aussi hanzoai/proofs.