Hanzo pubblica prove formali per l'infrastruttura degli agenti di IA

Oggi pubblichiamo in open source prove formali verificate dalla macchina per lo stack di infrastruttura di Hanzo AI. Non sono test né audit: sono garanzie matematiche controllate dal type checker di Lean 4.

Che cosa è dimostrato

Sicurezza degli agenti (6 prove)

• Limiti di capacità: un agente non può superare i permessi concessi
• Prevenzione dell'escalation: nessuna sequenza di azioni porta a una capacità non autorizzata
• Invocazione di strumenti MCP: la finestra di contesto si conserva tra una chiamata e l'altra
• Monotonia della delega: l'autorità delegata si restringe soltanto, non si allarga mai
• Ordine del flusso di lavoro: l'esecuzione del DAG rispetta gli archi di dipendenza
• Isolamento della memoria: il richiamo dell'agente è solo in aggiunta e limitato dalla rilevanza

Strato di calcolo (4 prove)

• Consenso Proof of AI: integrità della catena di attestazione TEE e convergenza del punteggio di qualità di fronte a guasti bizantini
• Calcolo confidenziale: isolamento dell'enclave e freschezza dell'attestazione
• Coordinamento dello sciame: equità nella distribuzione dei compiti e convergenza del bilanciamento del carico
• Correttezza della fatturazione: l'uso misurato non addebita mai di più

Gateway e piattaforma (6 prove)

• Validazione dei token, equità del limite di frequenza e correttezza della finestra scorrevole
• Sicurezza del rollback di un deploy blue-green e invariante di zero tempi di inattività
• Completezza della catena di fornitura della SBOM e monotonia del tracciamento delle vulnerabilità

KMS (1 prova)

• Applicazione della lista di accesso ai segreti: le chiavi master non attraversano mai il confine dell'HSM

I numeri

• 17 file Lean 4, 0 sorry, 0 errori di build
• 3 assiomi, tutti modellano confini hardware (isolamento TEE, perimetro dell'HSM, autenticazione esterna)
• Lean 4.14.0 + Mathlib 4.14.0, fissati e riproducibili
• Licenza Apache 2.0

Perché la verifica formale per gli agenti di IA

Gli agenti acquistano autonomia. Usano strumenti, gestiscono denaro, prendono decisioni. «Di solito funziona» non basta quando un agente ha accesso alle tue chiavi API, al tuo database e ai tuoi clienti.

La verifica formale dimostra che nessuna esecuzione possibile viola le proprietà di sicurezza. Non è «abbiamo provato 10.000 casi». Sono tutti. La prova che un agente non può elevare i privilegi non è probabilistica: è matematica.

Collegamenti

• Prove: github.com/hanzoai/proofs
• Articoli: github.com/hanzoai/papers — 34 articoli di ricerca dal 2014 al 2026
• Sito: proofs.hanzo.network

Il lavoro di verifica formale copre l'intero ecosistema Hanzo, dal gateway di IA all'infrastruttura degli agenti. Vedi anche hanzoai/proofs.