Anthropic يتحقق أمنياً من 123 مكتبة مفتوحة المصدر بواسطة Claude
كلّفت عملية التحقق إنتاج 180 مليون سطر من البراهين بصيغة Rocq، وكشفت مئات الأخطاء جرى إصلاحها وإعادة إثباتها.
أعلنت شركة Anthropic في 22 أكتوبر 2026 أنها استخدمت نموذج Claude للتحقق الشكلي من خصائص الأمان في 123 مكتبة مفتوحة المصدر مسجّلة في مشروع OSS-Fuzz التابع لـ Google، وذلك بالتعاون مع شركة Theorem المتخصصة في البراهين الشكلية، حسب aitimes.com.
وأنجز Claude براهين لـ 239 نقطة اختبار عبر المكتبات الـ123، تُظهر أن الاختبارات تنتهي دون أعطال لكل المدخلات التي تقل عن 64 ميغابايت، بما في ذلك انعدام أخطاء سلامة الذاكرة أو إخفاقات التأكيدات. وبلغ مجموع البراهين المولّدة 180 مليون سطر بصيغة مساعد البرهنة Rocq، بينما يغطي البرهان الوسيط ثنائياً بحجم نحو 18,000 تعليمة RISC-V.
وخلال عملية إثبات البراهين رصد Claude مئات الأخطاء، من بينها انخفاض غير صحيح في عدّاد داخل أداة فك ضغط، وقراءة خارج الحدود في مفكّك ترميز صور، ثم عدّل الشيفرة وأعاد إثبات صحة التعديلات. كما أعادت العملية اكتشاف الثغرة CVE-2026-56132 في مكتبة libexpat لتحليل XML.
وقالت Anthropic إن هذه أول عملية تحقق واسعة النطاق بواسطة الذكاء الاصطناعي من خصائص أمان برمجيات إنتاجية على مستوى شيفرة التجميع. ونشرت الشركة جزءاً من البراهين والنموذج المستخدم في التحقق، فيما تعرض Theorem دعماً لتطبيق العملية ذاتها على مشاريع مفتوحة المصدر أخرى.
تجربة منفصلة مع Opus 5.5
في تجربة أخرى، حلّ Opus 5.5 نصف 36 مهمة تحقق باستهلاك أقل بنحو 40% من الرموز المميزة (tokens) مقارنة بـ Opus 5، فيما خفّض تعاون الوكلاء استهلاك الرموز بنسبة 17%.
وكان التحقق الشكلي يُطبَّق في السابق أساساً على برمجيات حرجة للسلامة مثل أنظمة الطيران ونوى أنظمة التشغيل، لأنه يتطلب وقتاً وخبرة كبيرين؛ إذ استغرق التحقق من نواة seL4 الدقيقة سنتين من العمل للتنفيذ ونحو 20 سنة عمل شخصي للتحقق الشكلي. وفي تجارب سابقة لـ Anthropic، أظهر برهان على مستوى الشيفرة الثنائية أن تنفيذ ضغط zlib في نواة Linux مطابق لمواصفاته، كما جرى التحقق من مفسّر Python المكتوب بلغة Rust مقابل CPython بتطابق السلوك في 99.95% من أكثر من 1.7 مليون برنامج Python مولّد عشوائياً.
أسئلة سريعة
ما الذي أعلنت عنه Anthropic في 22 أكتوبر 2026؟
أنها استخدمت Claude، بالتعاون مع Theorem، للتحقق الشكلي من خصائص الأمان في 123 مكتبة مفتوحة المصدر من مشروع OSS-Fuzz، فأنجز 239 برهاناً ورصد مئات الأخطاء.
كم بلغ حجم البراهين المولّدة وبأي صيغة؟
بلغت 180 مليون سطر بصيغة مساعد البرهنة Rocq، ويغطي البرهان الوسيط ثنائياً بحجم نحو 18,000 تعليمة RISC-V.
هل نشرت Anthropic نتائج العمل؟
نشرت جزءاً من البراهين والنموذج المستخدم في التحقق، وتقدم Theorem دعماً لتطبيق العملية على مشاريع مفتوحة المصدر أخرى.