تغريدة بوريس تشيرني المنتشرة عن TLA+: ما الذي يتحقق منه النموذج الصوري فعلاً

استخدم بوريس تشيرني هذا الأسبوع نموذج Opus 5.5 لنمذجة أجزاء من Claude Agent SDK بلغتي TLA+ وLean، وفعلت الإنترنت ما تفعله دائماً: جمع المنشور نحو مليون مشاهدة وآلاف عمليات الحفظ، وتكرر في التعليقات سؤال واحد، ما هي TLA+ فعلاً؟ الأداة عمرها أكثر من 30 عاماً وتظهر باستمرار في الممارسة: كتبت Datadog مؤخراً عن وكلاء من نوع harness-first، بينما تُستخدم النماذج الصورية منذ زمن طويل في AWS وMongoDB وDatadog وKafka.

ما هي TLA+

TLA+ (Temporal Logic of Actions) لغة لكتابة أمرين: نظام انتقالات يصف ما يستطيع النظام فعله، وخصائص زمنية تصف ما يجب أن يتحقق في كل تشغيل. الحالات لقطات آنية (من مرشح، ومن صوّت لمن، ومن الزعيم)، والأفعال خطوات فردية بينها.

المثال الكلاسيكي هو انتخاب الزعيم: ثلاثة حواسيب، a وb وc، يجب أن تتفق على زعيم واحد، ولا يجوز وجود زعيمان في الوقت نفسه. تقول خصائص السلامة إن شيئاً سيئاً لا يحدث أبداً، بينما تقول خصائص liveness إن شيئاً جيداً سيحدث في النهاية، مثل انتخاب زعيم في نهاية المطاف. وتُكتب في TLA+ بثلاثة مؤثرات بسيطة: دائماً، وفي النهاية، وleads-to.

يتتبع مدقق النماذج القياسي TLC كل حالة يمكن الوصول إليها في نموذج منتهٍ، ويعيد مثالاً مضاداً عند انتهاك أي خاصية. وفي حالة ثلاثة حواسيب يكون الفضاء كله 38 حالة، أما مع تسعة فيتجاوز المليون.

ما ليست TLA+

ثمة ثلاث ملاحظات مهمة. يقتصر تدقيق النماذج على الحالات المنتهية، لذا يحتاج أي ادعاء عام إلى برهان، كما أن أداة البرهان الخاصة بـ TLA+، أي TLAPS، أتمتتها محدودة، خصوصاً في خصائص liveness. والمواصفة نموذج منفصل عن البرنامج: لا شيء يضمن أن التنفيذ يطابقها تماماً، وقد يتباعد الاثنان مع تغيّر الشيفرة. ولأن TLA+ تقوم على المنطق الزمني الخطي، فإن خصائص المستقبلات البديلة أو الاستراتيجيات، التي تعبّر عنها CTL وATL، تبقى خارج نطاقها.

من النماذج إلى براهين يتحقق منها الحاسوب

تذهب أنظمة البرهان الحديثة أبعد من ذلك. فـ Lean تفاعلية وعامة، وقد استُخدمت في منشور بوريس تشيرني؛ وVerus مبني حول Rust، لذا يمكن أن تعيش المواصفات والبراهين إلى جانب التنفيذ الحقيقي؛ ويستهدف Veil نماذج آلات الحالات، واستُخدم أخيراً للتحقق من محرك مزامنة، مصححاً 17 خطأً في الطريق.

يعمل فريق Reasonable على أتمتة جزء من هذا المسار. حوّل خط أنابيبهم 16,459 زوجاً حقيقياً من مواصفات وخصائص TLA+ إلى أكثر من 3,000 برهان Verus يتحقق منه الحاسوب: وكيل يكتب البرهان ووكيل آخر يراجعه، بينما يتحقق حارس منفصل من أن أياً منهما لم يغيّر المواصفة ولم يستخدم اختصارات مثل assume(false). الهدف برمجيات تُوصف وتُنفّذ وتُتحقق في حلقة واحدة.