I have been a member of the TLA+ project for over a decade, and I have the privilege to contribute to TLA+ as part of my day job. Besides working on its tools, I've been running the workshop/class on multiple occasions. Before getting involved with TLA+, I thought formal methods wouldn't be useful in practice, but first-hand experience convinced me otherwise.
I tweet at @lemmster.
TLA+, the temporal logic of actions, is a high-level specification language to design, document, and verify reactive systems. It has been around for two decades and is used in academia and by hardware-, and software-people at various companies. Its application spans the design of complex cloud systems, concurrent and distributed algorithms, processor hardware vulnerabilities (spectre/meltdown), ...
TLA+ has been described as a lightweight formal method, debuggable design, and the missing link between code and design documents.