أعلنت Google DeepMind في 10 نوفمبر 2026 استخدام إطارها الجديد للذكاء الاصطناعي، AlphaProof Code، للتحقق رسميًا من الشيفرة الفعلية لبروتوكول Signal. ويعني التحقق الرسمي إثباتًا رياضيًا أن البرنامج يعمل تمامًا كما هو مقصود، من دون أخطاء خفية. ووجّه الفريق وكلاء الذكاء الاصطناعي إلى إنشاء برهان والتحقق منه، لإثبات أن شيفرة Signal المترجمة تفرض ضمانات أمنية أساسية، مثل حماية الرسائل حتى إذا تعرض أحد الأجهزة للاختراق مؤقتًا. واستغرق العمل بأكمله أربعة أسابيع، وهي مهمة تتطلب عادةً سنوات من عمل فرق الخبراء.
ما الذي يفعله AlphaProof Code؟
AlphaProof Code نظام متعدد الوكلاء يعتمد على نماذج لغوية كبيرة (LLM). يبدأ الباحثون البشر بترجمة أهداف Signal الأمنية إلى مواصفات رسمية، مع مراجعة كل خطوة. بعد ذلك، تكتب مجموعة من الوكلاء، المدعومة بنموذج Gemini Carbon من DeepMind، البرهان بلغة Lean، وهي لغة تتحقق من النظريات الرياضية. وأنتج الوكلاء أكثر من ستة ملايين سطر من شيفرة Lean، ولم يحددوا سوى نحو واحد في المئة من قاعدة الشيفرة لمراجعتها بشريًا. كما تعرف النظام على نحو صحيح على خطأين أُصلحا سابقًا عند إعادة إدخالهما، ما يبين قدرته على التمييز بين الشيفرة الآمنة والمعيبة.
لماذا يُعد ذلك مهمًا؟
يشمل التحقق التنفيذ المترجم، لا التصميم وحده، ما يسد ثغرة تختبئ فيها كثير من نقاط الضعف في العالم الحقيقي. وقال إهرن كريت، كبير مسؤولي التكنولوجيا في Signal، إن النتيجة تمنح «ثقة أكبر في ضمانات الخصوصية في شيفرتنا». ويرى خبراء أن هذه خطوة نحو استخدام الذكاء الاصطناعي لتوفير مستوى متقدم من ضمانات الأمان للبنوك والأجهزة الطبية وبرمجيات شبكات الكهرباء وغيرها من الأنظمة الحيوية.
لماذا يهم
بالنسبة إلى المستخدمين، يعني هذا العمل أن التشفير الذي يحمي مليارات الرسائل في Signal وGoogle Messages خضع لفحص رياضي على مستوى التنفيذ، ما يقلل خطر وجود عيوب خفية. أما للمطورين، فيوضح نهجًا عمليًا لتسريع مراجعات الأمان باستخدام التحقق الرسمي بمساعدة الذكاء الاصطناعي، رغم أن تفاصيل التوسع على نطاق أوسع والتكلفة لا تزال غير واضحة.
