TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems.
There is an official TLA+ page which points to a whole lot of resources.
There is a Wikipedia page.
There is a 2015 CACM article on how TLA+ was intensively used at the time at Amazon Web Services:
Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. How Amazon web services uses formal methods. Commun. ACM 58, 4 (April 2015), 66–73. https://doi.org/10.1145/2699417
@article{10.1145/2699417,
author = {Newcombe, Chris and Rath, Tim and Zhang, Fan and Munteanu, Bogdan and Brooker, Marc and Deardeuff, Michael},
title = {How Amazon Web Services Uses Formal Methods},
year = {2015},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {58},
number = {4},
doi = {10.1145/2699417},
journal = {Communications of the ACM},
pages = {66–73},
}