TLA + هي لغة مواصفات رسمية طورها Leslie Lamport . تُستخدم لتصميم ونمذجة وتوثيق والتحقق من البرامج، خاصة الأنظمة المتزامنة والأنظمة المُوزعة . يُعتبر TLA + شيفرة زائفة قابلة للاختبار بشكل شامل، ويُشبه استخدامه برسم المخططات لأنظمة البرمجيات؛ TLA هو اختصار لـ Temporal Logic of Actions .في مجال التصميم والتوثيق، تؤدي لغة TLA + نفس دور المواصفات الفنية غير الرسمية.ومع ذلك، تُكتب مواصفات TLA +بلغة رسمية قائمة على المنطق والرياضيات، وتهدف دقة المواصفات المكتوبة بهذه اللغة إلى الكشف عن عيوب التصميم قبل البدء في تنفيذ النظام.
نظرًا لأن مواصفات TLA + تُكتب بلغة رسمية، فهي قابلة للفحص باستخدام تقنيات التحقق من النماذج المنتهية. يقوم مدقق النموذج باكتشاف جميع سلوكيات النظام الممكنة حتى عدد معين من خطوات التنفيذ، ويفحصها للكشف عن أي انتهاكات لخصائص الثبات المطلوبة مثل الأمان والحيوية . تستخدم مواصفات TLA + نظرية المجموعة الأساسية لتحديد الأمان (لن تحدث أشياء سيئة) والمنطق الزمني لتحديد الحيوية (تحدث أشياء جيدة في النهاية).تُستخدم لغة TLA + أيضًا لكتابة براهين صحة يتم التحقق منها آليًا لكل من الخوارزميات والنظريات الرياضية. تُكتب هذه البراهين بأسلوب إعلاني هرمي مستقل عن أي نظام إثبات معين. يمكن كتابة البراهين الرياضية المنظمة الرسمية وغير الرسمية بلغة TLA + ؛ حيث تشبه اللغة لغة LaTeX ، وتوجد أدوات لترجمة مواصفات TLA + إلى مستندات LaTeX.
تم تقديم لغة TLA + في عام 1999، بعد عدة عقود من البحث في طرق التحقق من صحة الأنظمة المتزامنة. ومُنذ ذلك الحين، تَم تطوير مجموعة أدوات متكاملة تشمل بيئة تطوير متكاملة IDE ومدقق النموذج الموزع.في عام 2009، تم إنشاء لغة البرمجة الشبيهة بالرمز PlusCal، وهي تنتقل إلى TLA + وهي مفيدة لتحديد الخوارزميات المتسلسلة. تم الإعلان عن TLA +2 في عام 2014، مما أدى إلى توسيع دعم اللغة لبناءات الإثبات. المرجع الحالي لـ TLA + هو The TLA + Hyperbook من تأليف Leslie Lamport.