Hanzo liefert formale Beweise für die Infrastruktur von KI-Agenten

Heute stellen wir maschinengeprüfte formale Beweise für den Infrastruktur-Stack von Hanzo AI als Open Source bereit. Das sind keine Tests und keine Audits. Es sind mathematische Garantien, die der Typprüfer von Lean 4 verifiziert.

Was bewiesen ist

Agentensicherheit (6 Beweise)

• Fähigkeitsgrenzen: Ein Agent kann erteilte Rechte nicht überschreiten
• Eskalationsschutz: Keine Aktionsfolge führt zu einer nicht erlaubten Fähigkeit
• MCP-Werkzeugaufruf: Das Kontextfenster bleibt über Aufrufe hinweg erhalten
• Monotonie der Delegation: Übertragene Befugnis wird nur enger, nie weiter
• Ablaufordnung: Die DAG-Ausführung achtet die Abhängigkeitskanten
• Speicherisolation: Die Erinnerung des Agenten ist nur anhängend und durch Relevanz begrenzt

Rechenschicht (4 Beweise)

• Proof-of-AI-Konsens: Integrität der TEE-Attestierungskette und Konvergenz der Qualitätsbewertung bei byzantinischen Fehlern
• Vertrauliches Rechnen: Enklavenisolation und Frische der Attestierung
• Schwarmkoordination: Faire Aufgabenverteilung und Konvergenz des Lastausgleichs
• Korrekte Abrechnung: Gemessene Nutzung berechnet nie zu viel

Gateway und Plattform (6 Beweise)

• Tokenprüfung, Fairness der Ratenbegrenzung und Korrektheit des gleitenden Fensters
• Sicheres Zurückrollen eines Blue-Green-Deployments und die Invariante ohne Ausfallzeit
• Vollständigkeit der SBOM-Lieferkette und Monotonie der Schwachstellenverfolgung

KMS (1 Beweis)

• Durchsetzung der Zugriffsliste für Geheimnisse: Hauptschlüssel überschreiten nie die HSM-Grenze

In Zahlen

• 17 Lean-4-Dateien, 0 sorry, 0 Baufehler
• 3 Axiome, alle modellieren Hardwaregrenzen (TEE-Isolation, HSM-Perimeter, externe Authentifizierung)
• Lean 4.14.0 + Mathlib 4.14.0, festgeschrieben und reproduzierbar
• Lizenz Apache 2.0

Warum formale Verifikation für KI-Agenten

Agenten werden selbstständiger. Sie benutzen Werkzeuge, verwalten Geld und treffen Entscheidungen. „Es funktioniert meistens“ reicht nicht, wenn ein Agent Zugriff auf Ihre API-Schlüssel, Ihre Datenbank und Ihre Kunden hat.

Formale Verifikation beweist, dass keine mögliche Ausführung die Sicherheitseigenschaften verletzt. Nicht „wir haben 10.000 Fälle getestet“. Alle. Der Beweis, dass ein Agent keine Rechte ausweiten kann, ist nicht wahrscheinlichkeitsbasiert. Er ist mathematisch.

Links

• Beweise: github.com/hanzoai/proofs
• Papiere: github.com/hanzoai/papers — 34 Forschungsarbeiten von 2014 bis 2026
• Seite: proofs.hanzo.network

Die formale Verifikation umfasst das ganze Hanzo-Ökosystem, vom KI-Gateway bis zur Agenteninfrastruktur. Siehe auch hanzoai/proofs.