تعاونت Anthropic مع Theorem Labs لدفع Claude إلى حملة واسعة بحثًا عن ثغرات البرمجيات بدقة تصل إلى مستوى كود الآلة. لقد أُنزل Claude إلى أعمق مستوى، للعمل على تعليمات التجميع RISC-V، وإجراء تحقق شكلي على عدد كبير من مستودعات الأكواد مفتوحة المصدر ذات المستوى الإنتاجي — وفي غضون أسابيع قليلة فقط، أنجز 123 مستودع مفتوح المصدر و239 نقطة اختبار، وأنتج 180 مليون سطر من أكواد البراهين الرياضية بلغة Rocq نجحت في التحقق.
ما يبعث على القلق الحقيقي هو ما كشفته. فالثغرات الخفية التي لم تتمكن الاختبارات الضبابية (fuzzing) على مدى مليارات المحاولات من اصطيادها، والزوايا المنطقية عالية الخطورة التي ظلت كامنة لأكثر من عشر سنوات، وحتى عيوب العتاد في مستوى معالجات x86 والأخطاء في الوثائق الرسمية، انتشلتها Claude دفعة واحدة. الاختبارات العشوائية التقليدية أشبه بغربلة الرمال مرارًا وتكرارًا بحثًا عن الثغرات، ودائمًا ما تفلت منها بعض الأسماك؛ أما روعة هذه الطريقة فهي أنها تحوّل نقاط الاختبار مباشرة إلى مقولات رياضية، وتقدم إثباتًا شاملًا يغطي جميع المسارات وجميع المدخلات — وبمجرد أن "يتعثر" الإثبات في موضع ما ويعجز عن التقدم، يكون ذلك الموضع غالبًا مخبأً للثغرة، كما أن Claude يستطيع في الوقت نفسه إصلاح الرقعة ثم مواصلة التحقق، مما خفّض معدل الثغرات المفوتة بشكل كبير.
وعند وضع الأمر على مقياس التكلفة يصبح معنى ذلك أوضح. فقد كان التحقق الشكلي بعمق كود الآلة في الماضي عملًا شاقًا معروفًا بكثافة هندسيته الضخمة، أما اليوم فبفضل قدرات النماذج اللغوية الضخمة يتضاعف كفاءة التحقق بمعدل يقارب الضعف كل شهرين تقريبًا، كما أن البراهين المكتوبة قابلة لإعادة الاستخدام عبر المشاريع. ووفق الاتجاه الحالي، يُقدَّر أن استثمار ما يقارب 134 مليون دولار سيجعل من الممكن بحلول نهاية 2027 إتمام التحقق من 95% من كود الآلة في منظومة Nix؛ وقد نُشرت بالفعل الدفعة الأولى من البراهين ذات الصلة. ومع تزايد ضغط الوضع الأمني السيبراني يومًا بعد يوم، يوفر هذا النهج المتمثل في "استخدام الذكاء الاصطناعي لتحويل صحة الأكواد إلى مبرهنات رياضية" خط دفاع جديدًا تمامًا للقطاع.