I've used it a bit for stuff inside Azure. It's difficult to find a problem where the model checker shines; state machines are far too simple (better to use P[1] or something similar), and something like cache coherence (the Hello World of real-world TLA+) isn't a problem I hit often.
TLA+ isn't only a model checker & theorem prover, though. The language itself is an excellent high-level way of expressing system design. Recently I've been applying it to eventually consistent systems, and writing an idea in TLA+ is a great way to flesh out the concept and spot hidden assumptions or edge cases. Lamport knows this; in the introduction to his TLA+ book, he quotes:
"Writing is nature's way of letting you know how sloppy your thinking is."
Followed by his own expansion on the concept:
"Our basic tool for writing specifications is mathematics. Mathematics is nature's way of letting you know how sloppy your writing is. ... The mathematics we use is more formal than the math you've grown up with. Formal mathematics is nature's way of letting you know how sloppy your mathematics is. The mathematics written by most mathematicians and scientists is not really precise. It's precise in the small, but imprecise in the large. Each equation is a precise assertion, but you have to read the accompanying words to understand how the equations relate to one another and exactly what the theorems mean. Logicians have developed ways of eliminating those words and making the mathematics completely formal and, hence, completely precise."
Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in.
You may also be interested in the AWS paper, which had excellent results.[2]
TLA+ isn't only a model checker & theorem prover, though. The language itself is an excellent high-level way of expressing system design. Recently I've been applying it to eventually consistent systems, and writing an idea in TLA+ is a great way to flesh out the concept and spot hidden assumptions or edge cases. Lamport knows this; in the introduction to his TLA+ book, he quotes:
"Writing is nature's way of letting you know how sloppy your thinking is."
Followed by his own expansion on the concept:
"Our basic tool for writing specifications is mathematics. Mathematics is nature's way of letting you know how sloppy your writing is. ... The mathematics we use is more formal than the math you've grown up with. Formal mathematics is nature's way of letting you know how sloppy your mathematics is. The mathematics written by most mathematicians and scientists is not really precise. It's precise in the small, but imprecise in the large. Each equation is a precise assertion, but you have to read the accompanying words to understand how the equations relate to one another and exactly what the theorems mean. Logicians have developed ways of eliminating those words and making the mathematics completely formal and, hence, completely precise."
Most of the value I get from TLA+ is as a software design tool. It's also just a fun language to write stuff in.
You may also be interested in the AWS paper, which had excellent results.[2]
[1] https://plang.codeplex.com
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/am...