المواصفات الشكلية أدوات للحوادث، لا براهين أكاديمية

هناك لحظة في كل حادث حقيقي يتوقف فيها النقاش عن الميزات ويبدأ الحديث عن الوقت.

وقت لإيقاف النزف. وقت لفهم الحالة التي يوجد عليها النظام. وقت لاتخاذ قرار: هل إعادة التشغيل تحسّن الوضع أم توسّع نطاق الضرر؟ وقت للإجابة عن السؤال الوحيد الذي سيكرهك عليه نفسك في المستقبل إن تجاهلته: «إذا لم نفعل شيئًا، ماذا سيحدث بعد ذلك؟»

في تلك اللحظة تتحول معظم الأنظمة الموزعة إلى مسابقة سرد. لدى الجميع رواية تبدو معقولة. ولا يمكن دحض أي رواية بسرعة كافية.

لهذا أعود دائمًا إلى المواصفات الشكلية. ليس كاختبار للنقاء. بل كأداة لإدارة الحوادث.

قال Hillel Wayne ذلك بوضوح في حواره الأخير حول الأساليب الشكلية: الأساليب الشكلية ليست فقط لإثبات صحة البرامج، بل لجعل الأجزاء الحرجة من الأنظمة دقيقة بما يكفي كي يمكن الاستدلال عليها. هذه الدقة هي الفارق بين «نعتقد» و«نعرف»، خصوصًا عندما يكون النظام موزعًا ومؤتمتًا وتحت حمل.

المشكلة الحقيقية ليست الأخطاء. بل الحالة التي لا تستطيع تفسيرها.

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

والآن أضف الوكلاء.

سير عمل agentic ليس مجرد كود يعمل. إنه كود يقرر، ثم يتخذ إجراءات تخلق مزيدًا من الحالة. إذا استدعى خدمات خارجية، أو فعّل مدفوعات، أو وضع أوامر، أو حدّث استحقاقات العملاء، فإن كل إجراء يصبح جزءًا من سلسلة قد تضطر لتبريرها لاحقًا.

عندما تسوء الأمور، نادرًا ما يكون نمط الفشل «تعطّل». غالبًا يكون «استمرّ، لكن ضمن واقع خاطئ».

• عاملان يعتقد كل منهما أنه يملك المهمة نفسها.
• إعادة محاولة تحوّل إجراءً يُفترض أن يحدث مرة واحدة إلى إجراء يحدث «مرة واحدة على الأقل».
• إنسان يرى لوحة مؤشرات ذات اتساق نهائي ويتخذ قرارًا بناءً على حالة شبحية.
• وكيل يقرأ سياقًا قديمًا وينفّذ بثقة إجراءً صحيحًا في توقيت خاطئ.

الاختبارات التقليدية لا تغطي ذلك جيدًا لأنك لا تستطيع تعداد التداخلات التنفيذية التي تهم فعلاً. الرصد التشغيلي يساعدك على رؤية ما حدث، لكن بعد وقوعه. «لدينا سجلات» ليست مساوية لـ«لدينا نموذج».

المواصفات الشكلية، وبالأخص TLA+، تجبرك على تعريف النظام كآلة حالات: ما الحالات الموجودة، ما الانتقالات المسموح بها، وما الذي يجب أن يظل صحيحًا دائمًا. هذا ليس أكاديميًا. هذه هي الطريقة الوحيدة التي أعرفها لجعل سلوك الأنظمة الموزعة مقروءًا ومفهومًا.

الحتمية ليست تفصيلاً تنفيذيًا. إنها متطلب أعمال.

في أنظمة التداول وما يجاور المدفوعات، الهدف ليس «لا حوادث». الهدف هو «ضرر محدود، نتائج قابلة للتفسير، واستعادة سريعة». يمكن التعايش مع تعطل مكوّن. لا يمكن التعايش مع عدم معرفة ما الذي فعله.

الحتمية، عمليًا، تعني أربعة أمور:

1. Idempotence مُعرّفة بوضوح: تقرر أي الإجراءات يمكن تكرارها بأمان، وتشفّر المفتاح الذي يجعلها آمنة.
2. الترتيب مقصود: تختار أين يهم الترتيب (لكل حساب، لكل محفظة، لكل عميل)، وأين لا يهم.
3. الملكية أحادية: جهة واحدة تقرر، والبقية تراقب. وإذا كانت جهات متعددة تقرر، فأنت تنمذج آلية التحكيم.
4. الثوابت غير قابلة للتفاوض: تحدد ما الذي يجب ألا يحدث مطلقًا، حتى أثناء إعادات المحاولة، أو backfills، أو الانقطاعات الجزئية.

هذه هي النقلة الذهنية نفسها التي تجعل أنظمة الذكاء الاصطناعي أكثر أمانًا. ليس لأن الذكاء الاصطناعي سحر، بل لأنه احتمالي. إذا سمحت لمكوّنات احتمالية بأن تكتب مباشرة في «حقيقتك المالية» أو في نظام السجل لديك، ستفقد القدرة على إعادة التشغيل والدفاع عن النتائج. ضعها في طبقة السرد، وأبقِ طبقة الحقيقة حتمية. (هذا الفصل قريب مما ناقشته في LLMs Belong in the Narrative Layer, Not in the Financial Truth Layer.)

المواصفات الشكلية تقع تحديدًا على هذا الحد. إنها طريقة لتثبيت النواة الحتمية وثوابتها، كي يستطيع باقي النظام أن يكون خلاقًا دون أن يكون خطِرًا.

ما الذي تمنحك إياه TLA+ تحت ضغط الحوادث

القيمة الأقل تقديرًا في TLA+ ليست model checker. بل الحوار الذي تفرضه.

عندما تكتب مواصفة، لا مكان يختبئ فيه الغموض. لا يمكنك أن تقول «العامل يلتقط المهمة». يجب أن تعرّف متى تصبح مؤهلة، ومن يحق له المطالبة بها، وماذا يحدث إن حاول عاملان ذلك. ولا يمكنك أن تقول «نُجري تسوية لاحقًا». يجب أن تعرّف انتقال التسوية وما الذي يُسمح له بتغييره.

تحت ضغط الحوادث، هذه الدقة تعود عليك بثلاث فوائد ملموسة:

• قابلية التدقيق: يمكنك ربط الأحداث المرصودة بانتقالات مسموح بها. إذا حدث شيء غير موجود في النموذج، لديك عيب حقيقي لا لغزًا.
• قابلية الاستعادة: يمكنك تصميم «حركات الإصلاح» مسبقًا. backfill وreplay وعمليات التعويض ومسارات التجميد هي انتقالات أيضًا. إذا لم تنمذجها، سترتجلها في أكثر الأوقات كلفة.
• ضبط نطاق الضرر: الثوابت تخبرك بما يمكنك تخفيفه بأمان وما يجب حمايته بأي ثمن. هذا الوضوح أفضل من البطولات الفردية.

هذا يتسق مع تأكيد Wayne أن الأساليب الشكلية أصبحت أكثر عملية، وأن أدوات مثل TLA+ تُستخدم لأنها تساعد الفرق على الاستدلال حول سلوك معقد، لا لأنها تنتج برمجيات مثالية. هذا التأطير البراغماتي هو ما يهم في سياق الأعمال. أنت لا تشتري يقينًا. أنت تشتري «مجهولات أقل من النوع الذي لا تعرف أنك تجهله». (وللمرة الثانية، راجع النقاش.)

نمط معيش: الحادث الذي يصبح فيه «لا نستطيع الجزم» هو الانقطاع الحقيقي

بنيت أتمتة للتداول لم يكن فيها الكود هو الجزء المخيف. الجزء المخيف كان العقد غير المرئي بين المكوّنات: من المخوّل بالتصرف، وتحت أي شروط مسبقة، وكيف نعرف أن الإجراء نهائي.

فئة واحدة من الحوادث كانت تتكرر عبر أنظمة وفرق مختلفة: النظام فعل ما كان «مسموحًا» له محليًا، لكنه عالميًا خالف المقصود. إعادة محاولة انطلقت بعد timeout، وإقرار وصل متأخرًا، وخدمتان اختلفتا حول ما إذا كان انتقال الحالة قد تم تثبيته. الانقطاع لم يكن توقفًا عن العمل. الانقطاع كان عدم اليقين.

عندما لا تستطيع الجزم إن كان انتقال حالة قد حدث، لا يمكنك المتابعة بأمان. تتجمد. يبدأ البشر بتشغيل سكربتات يدوية. يقترح الناس إعادة تشغيل الطوابير وإعادة نشر الخدمات لأن هذه هي الرافعات الوحيدة التي يرونها. وفي الوقت نفسه يواصل النظام الانحراف.

المواصفة الشكلية لم تكن لتمنع كل إخفاق. لكنها كانت ستجعل أمرين واضحين بلا لبس:

• الثوابت الدقيقة التي تُعرّف سلوكًا «صحيحًا بما يكفي».
• الانتقالات الدقيقة التي تُعدّ خطوات استعادة آمنة، بما في ذلك ما هو محظور.

هذا ما أعنيه حين أقول إنها أداة للحوادث. إنها طريقة لتقليص مساحة الارتجال.

كيف تتبنى المواصفات الشكلية دون تحويلها إلى عرض شكلي

لا تحتاج إلى برنامج تحقق شكلي على مستوى الشركة. تحتاج إلى نقطة ضيقة واحدة يكون فيها الغموض مكلفًا.

إليك نمطًا يعمل مع فرق حقيقية:

1) اختر «سير عمل الحقيقة» واحدًا وارسم الحد

اختر سير عمل تكون فيه الحالة الخاطئة أسوأ من التوقف. أمثلة: الاستحقاقات، حالة الفوترة، دورة حياة الطلب، مراكز المحافظ، المدفوعات الخارجة، الآثار الجانبية غير القابلة للعكس.

حدد ما هو داخل النواة الحتمية (آلة الحالات، الثوابت، الانتقالات)، وما هو خارجها (UI، التحليلات، استدلال الوكيل، التوصية).

2) اكتب المواصفة قبل إعادة البناء التالية، لا بعد الحادث

المواصفات التي تُكتب بعد post-mortem غالبًا تتحول إلى توثيق. المواصفات التي تُكتب قبل البناء تتحول إلى تصميم.

اجعلها صغيرة. إذا كانت كبيرة إلى درجة لا يمكن معها تشغيل model-checking، فهي كبيرة إلى درجة تجعلها غير مفيدة كأداة قرار.

3) نمذج حركات الفشل كانتقالات من الدرجة الأولى

معظم الأنظمة تنمذج المسار السعيد ثم «تتعامل مع الأخطاء». هذا غير كافٍ.

• ماذا يعني «التجميد» بمصطلحات الحالة؟
• كيف تستأنف دون تطبيق الإجراءات مرتين؟
• كيف يبدو التعويض، وما الذي لا يجب أن يلمسه مطلقًا؟

هذه هي العقلية نفسها وراء بناء rollouts للذكاء الاصطناعي تتراكم آثارها: تصنع مسارًا مضبوطًا من الواقع الحالي إلى الواقع المستهدف، مع قابلية للرجوع حيثما أمكن. (ذو صلة: Build on the Stack You Have: The Rollout Pattern That Makes AI Compound.)

4) حوّل الثوابت إلى فحوصات تشغيلية وrunbooks

مواصفة تعيش في repo ولا تمس سلوك الإنتاج لن يطول بها الأمر حتى تُنسى.

اختر 3 إلى 5 ثوابت ونفّذها على شكل:

• assertions تشغيلية أو حواجز على الحدود.
• تنبيهات تستدعي البشر عند خرق ثابت، لا عند أعراض ضجيجية.
• خطوات runbook تُحيل إلى الثابت: ما الذي تفحصه، ما الذي تجمّده، ما الذي تعيد تشغيله.

5) تعامل مع المواصفة كـ governance للتغيير

أي تغيير يؤثر في سير عمل الحقيقة ينبغي أن يحدّث المواصفة أولًا. هذا شكل خفيف من ضبط التغيير لا يبطئ الفرق؛ بل يمنع التراجع المكلف.

تجاوزات الميزانية في البرمجيات غالبًا تأتي من بناء الشيء الخطأ مرتين. الديناميكية نفسها تنطبق هنا: الغموض مركز تكلفة. (وإذا أردت زاوية governance الأوسع، راجع Budget overruns are rarely a surprise. They are a governance choice.)

رأيي: الذكاء الاصطناعي لن يلغي الحاجة إلى المواصفات. بل سيرفع كلفة غيابها.

هناك فكرة مغرية في خلفية موجة الذكاء الاصطناعي الحالية: أن النماذج ستكتب الكود، وربما تتحقق منه أيضًا. يتطرق Wayne إلى ما إذا كان الذكاء الاصطناعي قد يجعل الأساليب الشكلية سائدة، وأنا أتفق مع الاتجاه لا مع القراءة الكسولة. (راجع المقابلة.)

إذا جعل الذكاء الاصطناعي إنتاج البرمجيات أرخص، فإنه يجعل أيضًا إنتاج أنماط فشل دقيقة أرخص. الأنظمة agentic تضاعف الآثار الجانبية. الأنظمة الموزعة تضاعف التداخلات. ومعًا يضاعفان عدد الروايات المعقولة خلال الانقطاع.

المواصفات الشكلية هي كيف تُبقي جزءًا من النظام مملًا. حتميًا. قابلًا للتدقيق. قابلًا للاستعادة. هذا ليس ترفًا. هذا هو الأساس الذي يسمح لك بالتحرك بسرعة في كل مكان آخر.

استخدم TLA+ حيث يمكن أن تتحول عبارة «لا نستطيع الجزم» إلى أسوأ حادث لديك. إذا لم تستطع تفسير الحالة، فأنت لا تملك النظام.

هذا رأيي، ولم أرَ بعد فريقًا ندم لأنه جعل سير عمل الحقيقة قابلًا للفهم.