Hanzo تنشر براهين صورية لبنى وكلاء الذكاء الاصطناعي

نفتح اليوم مصدر البراهين الصورية التي تتحقق منها الآلة لمكدس بنية Hanzo AI. ليست اختبارات ولا عمليات تدقيق. إنها ضمانات رياضية يفحصها مدقق الأنواع في Lean 4.

ما الذي أُثبت

سلامة الوكلاء (6 براهين)

• حدود القدرة: لا يستطيع الوكيل تجاوز الأذونات الممنوحة
• منع التصعيد: لا يؤدي أي تسلسل من الأفعال إلى قدرة غير مصرح بها
• استدعاء أدوات MCP: تُحفظ نافذة السياق عبر الاستدعاءات
• اطّراد التفويض: السلطة المفوضة تضيق فقط ولا تتسع أبدًا
• ترتيب سير العمل: تنفيذ DAG يحترم حواف الاعتماد
• عزل الذاكرة: استذكار الوكيل للإلحاق فقط ومحدود بالصلة

طبقة الحوسبة (4 براهين)

• إجماع Proof of AI: سلامة سلسلة توثيق TEE وتقارب تقييم الجودة عند الأعطال البيزنطية
• الحوسبة السرية: عزل الجيب وحداثة التوثيق
• تنسيق السرب: عدالة توزيع المهام وتقارب موازنة الحمل
• صحة الفوترة: الاستخدام المقاس لا يبالغ في التحصيل أبدًا

البوابة والمنصة (6 براهين)

• التحقق من الرموز، وعدالة حد المعدل، وصحة النافذة المنزلقة
• سلامة التراجع في نشر blue-green وثابت انعدام التوقف
• اكتمال سلسلة توريد SBOM واطّراد تتبع الثغرات

KMS (برهان واحد)

• إنفاذ قائمة الوصول إلى الأسرار: المفاتيح الرئيسية لا تعبر حدود HSM أبدًا

بالأرقام

• 17 ملف Lean 4، بلا sorry، وبلا أخطاء بناء
• 3 مسلمات، كلها تنمذج حدود العتاد (عزل TEE، ومحيط HSM، والمصادقة الخارجية)
• Lean 4.14.0 + Mathlib 4.14.0، مثبتة وقابلة لإعادة الإنتاج
• ترخيص Apache 2.0

لماذا التحقق الصوري لوكلاء الذكاء الاصطناعي

يزداد الوكلاء استقلالًا. يستخدمون الأدوات ويديرون المال ويتخذون القرارات. «يعمل عادة» لا يكفي حين يملك الوكيل مفاتيح API وقاعدة بياناتك وعملاءك.

يثبت التحقق الصوري أن أي تنفيذ ممكن لا يخرق خصائص السلامة. ليس «اختبرنا 10,000 حالة». بل كلها. البرهان على أن الوكيل لا يستطيع رفع امتيازاته ليس احتماليًا. إنه رياضي.

روابط

• البراهين: github.com/hanzoai/proofs
• الأوراق: github.com/hanzoai/papers — 34 ورقة بحثية من 2014 إلى 2026
• الموقع: proofs.hanzo.network

يغطي عمل التحقق الصوري منظومة Hanzo كلها، من بوابة الذكاء الاصطناعي إلى بنية الوكلاء. انظر أيضًا hanzoai/proofs.