TLA+

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.

References

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},
}