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