الأسبوع الماضي، ذكر Boris Cherny، مخترع Claude Code، أن Opus كان قادرًا على استخدام TLA+ للعثور على حالات السباق في الكود. الآن الجميع يتحدث عن التحقق الرسمي. كمعلم طويل الأمد وداعم لـ TLA+، هذا مثير. لكن النشوة الجديدة تقلقني. لن تحل الأساليب الرسمية مشكلة تطوير البرمجيات الوكيلة مرة واحدة وإلى الأبد.

التصاميم الصحيحة لا تترجم تلقائيًا إلى كود صحيح. للتحقق من خاصية، نحتاج إلى خاصية للتحقق منها. يقسم TLA+ النظام إلى سلوكيات، كل منها سلسلة من الحالات. في كل حالة يمكننا التعبير عن تعبيرات منطقية بثلاثة عوامل زمنية: `[]P` (دائمًا P)، `P'` (P في الحالة التالية)، و `<>P` (في النهاية P).

`[]P` تعني أن P صحيح في كل حالة من كل سلوك، ويسمى ثابتًا. `[](x' >= x)` هي خاصية فعل. هذه هي خصائص السلامة: شيء سيء لا يحدث أبدًا. تستخدم خصائص الحيوية `<>`: `[]<>P` تعني أن P صحيح في حالة مستقبلية واحدة على الأقل من كل حالة؛ `<>[]P` تعني أن P يصبح صحيحًا ويبقى صحيحًا إلى الأبد؛ `[](P => <>Q)` تعني أن P يسبب Q في النهاية.