Cette thèse porte sur TLA+, un langage de spécification fondé sur la logique temporelle et la théorie des ensembles non typée. TLA+ est principalement utilisé dans l’industrie pour vérifier des systèmes concurrents et distribués. On s’intéresse en particulier à la preuve interactive de théorèmes TLA+, qui peut être réalisée avec l’outil TLAPS. Cet assistant de preuve emploie une batterie de prouveurs automatiques externes afin de vérifier les obligations de preuve qui correspondent aux étapes de raisonnement de l’utilisateur.