Hanzo เผยแพร่บทพิสูจน์เชิงรูปนัยสำหรับโครงสร้างพื้นฐานเอเจนต์ AI

วันนี้เราเปิดซอร์สบทพิสูจน์เชิงรูปนัยที่เครื่องตรวจแล้วสำหรับกองโครงสร้างพื้นฐานของ Hanzo AI สิ่งเหล่านี้ไม่ใช่การทดสอบหรือการตรวจสอบบัญชี แต่เป็นหลักประกันทางคณิตศาสตร์ที่ตัวตรวจชนิดของ Lean 4 ยืนยัน

สิ่งที่พิสูจน์แล้ว

ความปลอดภัยของเอเจนต์ (6 บทพิสูจน์)

• ขอบเขตความสามารถ: เอเจนต์เกินสิทธิ์ที่ได้รับไม่ได้
• การกันไม่ให้ยกระดับ: ไม่มีลำดับการกระทำใดนำไปสู่ความสามารถที่ไม่ได้รับอนุญาต
• การเรียกเครื่องมือ MCP: หน้าต่างบริบทคงอยู่ข้ามการเรียก
• ความทางเดียวของการมอบอำนาจ: อำนาจที่มอบไปได้แต่แคบลง ไม่กว้างขึ้น
• ลำดับงาน: การทำงานของ DAG เคารพเส้นความขึ้นต่อ
• การแยกหน่วยความจำ: ความจำของเอเจนต์เพิ่มได้อย่างเดียวและถูกจำกัดด้วยความเกี่ยวข้อง

ชั้นคำนวณ (4 บทพิสูจน์)

• ฉันทามติ Proof of AI: ความสมบูรณ์ของสายรับรอง TEE และการลู่เข้าของคะแนนคุณภาพเมื่อมีความผิดพร่องแบบไบแซนไทน์
• การคำนวณที่เป็นความลับ: การแยก enclaves และความสดของการรับรอง
• การประสานฝูง: ความเป็นธรรมในการแจกงานและการลู่เข้าของการถ่วงโหลด
• ความถูกต้องของการคิดเงิน: การใช้ที่วัดได้ไม่คิดเงินเกิน

เกตเวย์และแพลตฟอร์ม (6 บทพิสูจน์)

• การตรวจโทเคน ความเป็นธรรมของขีดอัตรา และความถูกต้องของหน้าต่างเลื่อน
• ความปลอดภัยของการย้อนกลับการนำขึ้นแบบ blue-green และค่าคงที่ไร้เวลาหยุด
• ความครบของห่วงโซ่อุปทาน SBOM และความทางเดียวของการติดตามช่องโหว่

KMS (1 บทพิสูจน์)

• การบังคับรายการเข้าถึงความลับ: คีย์หลักไม่ข้ามขอบ HSM

เป็นตัวเลข

• ไฟล์ Lean 4 จำนวน 17 ไฟล์, sorry เป็น 0, ข้อผิดพลาดตอนสร้างเป็น 0
• สัจพจน์ 3 ข้อ ทั้งหมดจำลองขอบฮาร์ดแวร์ (การแยก TEE, ขอบเขต HSM, การยืนยันตัวตนภายนอก)
• Lean 4.14.0 + Mathlib 4.14.0 ปักไว้และทำซ้ำได้
• สัญญาอนุญาต Apache 2.0

เหตุใดจึงตรวจเชิงรูปนัยสำหรับเอเจนต์ AI

เอเจนต์มีอิสระมากขึ้น ใช้เครื่องมือ จัดการเงิน และตัดสินใจ «มักจะใช้ได้» ไม่พอเมื่อเอเจนต์ถือคีย์ API ฐานข้อมูล และลูกค้าของคุณ

การตรวจเชิงรูปนัยพิสูจน์ว่า ไม่มีวิถีปฏิบัติที่เป็นไปได้ใด ละเมิดสมบัติความปลอดภัย ไม่ใช่ «เราทดสอบ 10,000 กรณี» แต่คือทั้งหมด บทพิสูจน์ว่าเอเจนต์ยกระดับสิทธิ์ไม่ได้ไม่ใช่ความน่าจะเป็น มันคือคณิตศาสตร์

ลิงก์

• บทพิสูจน์: github.com/hanzoai/proofs
• บทความ: github.com/hanzoai/papers — บทความวิจัย 34 ฉบับตั้งแต่ 2014 ถึง 2026
• ไซต์: proofs.hanzo.network

งานตรวจเชิงรูปนัยครอบคลุมระบบนิเวศ Hanzo ทั้งหมด ตั้งแต่เกตเวย์ AI จนถึงโครงสร้างพื้นฐานเอเจนต์ ดูเพิ่มที่ hanzoai/proofs