فريق Frontier Red Team في Anthropic يثبت رياضيًا خلوّ 239 نقطة دخول في مكتبات مفتوحة المصدر من الـ crash

نشر فريق Frontier Red Team في Anthropic في 22 أكتوبر 2026 نتائج عمل مشترك مع شركة Theorem، يكتب فيه الموديل إثباتًا رياضيًا بأن الكود لا يمكن أن يتوقف بـ crash، بدل تجربة مدخلات عشوائية على أمل العثور على خطأ. ومن بين النتائج أن قارئ PDF واحدًا خرج منه في أسبوع عدد من الثغرات يساوي ما يُبلَّغ عنه فيه خلال سنة كاملة.

وشمل العمل 239 نقطة دخول في 123 مكتبة مفتوحة المصدر، أُثبت أنها لا تتوقف بـ crash على أي مدخل أصغر من 64 ميجابايت. وبلغ حجم الإثباتات نحو 180 مليون سطر بلغة Rocq، أي قرابة 600,000 سطر للإثبات الواحد في المتوسط. واستغرق العمل كله أسابيع قليلة، وعثر الموديل في الطريق على مئات الأخطاء وأصلحها.

وفي تجربة ثانية، أُثبت مفسّر Python مكتوب بـ Rust باستخدام أداة Verus، ثم جُرّب على 1.7 مليون برنامج عشوائي، فطابق سلوكه CPython في 99.95% من الحالات.

والفرق بين الطريقتين جوهري. فالاختبار التقليدي يجرّب حالات بعينها، ولا يقول شيئًا عن الحالات التي لم يجرّبها. أما الإثبات الرسمي فيبرهن أن خاصية ما صحيحة لكل مدخل ضمن الحدود المعلنة، ويتحقق مدقق مثل Rocq من صحة البرهان آليًا.

وتكتب Anthropic حدود النتائج بنفسها: عبارة “formally verified” لا تعني أن الكود خالٍ من الأخطاء، والإثباتات مبنية على binary ثابت single-threaded لمعمارية RISC-V مع musl libc، بينما تعمل أغلب المنتجات المنشورة على x86 أو ARM مع glibc. فالنتائج لا تنتقل إليها مباشرة.

والذي تغيّر إذن هو التكلفة لا النطاق. وقد نشرت Theorem مهارة (skill) لـ Claude تساعد على تجربة الطريقة على كود آخر، وتعرض تشغيل الـ pipeline على مشاريع مفتوحة المصدر أخرى. ويخص ذلك أكثر من غيره من يكتبون كود parsing أو يستقبلون ملفات من مصادر خارجية.