Hanzo merilis bukti formal untuk infrastruktur agen AI

Hari ini kami membuka sumber bukti formal yang diperiksa mesin untuk tumpukan infrastruktur Hanzo AI. Ini bukan pengujian atau audit. Ini jaminan matematika yang diverifikasi pemeriksa tipe Lean 4.

Yang terbukti

Keamanan agen (6 bukti)

• Batas kemampuan: agen tidak dapat melampaui izin yang diberikan
• Pencegahan eskalasi: tidak ada urutan tindakan yang menuju kemampuan tanpa izin
• Pemanggilan alat MCP: jendela konteks terjaga antar panggilan
• Monotonitas delegasi: wewenang yang didelegasikan hanya menyempit, tidak pernah melebar
• Urutan alur kerja: eksekusi DAG menghormati sisi ketergantungan
• Isolasi memori: ingatan agen hanya bertambah dan dibatasi relevansi

Lapisan komputasi (4 bukti)

• Konsensus Proof of AI: keutuhan rantai atestasi TEE dan konvergensi skor kualitas di bawah kesalahan Bizantium
• Komputasi rahasia: isolasi enklave dan kesegaran atestasi
• Koordinasi kawanan: keadilan distribusi tugas dan konvergensi penyeimbang beban
• Ketepatan penagihan: pemakaian terukur tidak pernah menagih lebih

Gerbang dan platform (6 bukti)

• Validasi token, keadilan batas laju, dan ketepatan jendela geser
• Keamanan pengembalian deploy blue-green dan invarian tanpa waktu henti
• Kelengkapan rantai pasok SBOM dan monotonitas pelacakan kerentanan

KMS (1 bukti)

• Penegakan daftar akses rahasia: kunci master tidak pernah melewati batas HSM

Dalam angka

• 17 berkas Lean 4, 0 sorry, 0 galat bangun
• 3 aksioma, semuanya memodelkan batas perangkat keras (isolasi TEE, perimeter HSM, autentikasi eksternal)
• Lean 4.14.0 + Mathlib 4.14.0, disematkan dan dapat direproduksi
• Berlisensi Apache 2.0

Mengapa verifikasi formal untuk agen AI

Agen makin otonom. Mereka memakai alat, mengelola uang, dan mengambil keputusan. «Biasanya berhasil» tidak cukup ketika agen memegang kunci API, basis data, dan pelanggan Anda.

Verifikasi formal membuktikan bahwa tidak ada eksekusi yang mungkin melanggar sifat keamanan. Bukan «kami menguji 10.000 kasus». Semuanya. Bukti bahwa agen tidak dapat menaikkan hak istimewa bukanlah probabilitas. Itu matematika.

Tautan

• Bukti: github.com/hanzoai/proofs
• Makalah: github.com/hanzoai/papers — 34 makalah penelitian dari 2014 sampai 2026
• Situs: proofs.hanzo.network

Kerja verifikasi formal mencakup seluruh ekosistem Hanzo, dari gerbang AI sampai infrastruktur agen. Lihat juga hanzoai/proofs.