Hanzo, yapay zeka ajanı altyapısı için biçimsel kanıtlar yayımladı

Bugün Hanzo AI altyapı yığını için makineyle doğrulanmış biçimsel kanıtları açık kaynak olarak açıyoruz. Bunlar test ya da denetim değil. Lean 4 tür denetleyicisinin doğruladığı matematiksel güvenceler.

Neyin kanıtlandığı

Ajan güvenliği (6 kanıt)

• Yetki sınırları: bir ajan verilen izinleri aşamaz
• Yükseltmenin önlenmesi: hiçbir eylem dizisi yetkisiz bir yeteneğe varmaz
• MCP araç çağrısı: bağlam penceresi çağrılar arasında korunur
• Yetki devrinin tekdüzeliği: devredilen yetki yalnızca daralır, hiç genişlemez
• İş akışı sırası: DAG yürütmesi bağımlılık kenarlarına uyar
• Bellek yalıtımı: ajanın anımsaması yalnızca eklemelidir ve ilgililikle sınırlıdır

Hesaplama katmanı (4 kanıt)

• Proof of AI uzlaşısı: TEE tasdik zincirinin bütünlüğü ve Bizans hatalarında kalite puanının yakınsaması
• Gizli hesaplama: enklav yalıtımı ve tasdiğin tazeliği
• Sürü eşgüdümü: görev dağıtımında adalet ve yük dengelemenin yakınsaması
• Faturalamanın doğruluğu: ölçülen kullanım hiçbir zaman fazla ücretlendirmez

Ağ geçidi ve platform (6 kanıt)

• Jeton doğrulama, hız sınırının adaleti ve kayan pencerenin doğruluğu
• Blue-green dağıtımında geri alma güvenliği ve sıfır kesinti değişmezi
• SBOM tedarik zincirinin eksiksizliği ve güvenlik açığı izlemenin tekdüzeliği

KMS (1 kanıt)

• Gizli erişim listesinin uygulanması: ana anahtarlar HSM sınırını hiç geçmez

Sayılarla

• 17 Lean 4 dosyası, 0 sorry, 0 derleme hatası
• 3 aksiyom, hepsi donanım sınırlarını modeller (TEE yalıtımı, HSM çevresi, dış kimlik doğrulama)
• Lean 4.14.0 + Mathlib 4.14.0, sabitlenmiş ve yeniden üretilebilir
• Apache 2.0 lisansı

Yapay zeka ajanları için neden biçimsel doğrulama

Ajanlar özerklik kazanıyor. Araç kullanıyor, para yönetiyor, karar veriyorlar. Bir ajanın API anahtarlarınıza, veritabanınıza ve müşterilerinize erişimi varken «genellikle çalışır» yetmez.

Biçimsel doğrulama, olası hiçbir yürütmenin güvenlik özelliklerini çiğnemediğini kanıtlar. «10.000 durumu denedik» değil. Hepsi. Bir ajanın yetkilerini yükseltemeyeceğinin kanıtı olasılıksal değildir. Matematikseldir.

Bağlantılar

• Kanıtlar: github.com/hanzoai/proofs
• Makaleler: github.com/hanzoai/papers — 2014-2026 arasını kapsayan 34 araştırma makalesi
• Site: proofs.hanzo.network

Biçimsel doğrulama çalışması, yapay zeka ağ geçidinden ajan altyapısına kadar tüm Hanzo ekosistemini kapsar. Ayrıca bkz. hanzoai/proofs.