[2muchcoffeeman]

> I disagree. Amazon has had great success employing TLA+ in finding bugs, testing design changes, and chasing aggressive optimizations [0].

I googled TLA+ examples and tutorials and I am wondering how I would apply this to an already existing application?

[agentultra]

I look for the critical bottlenecks in the application where the cost of failure or mistakes is fairly high. This is where I feel I will get the most "bang for the buck" so to speak.

You don't have to specify the entire application to get the benefit of high level specifications. Even specifying the protocol between two communicating channels can bring benefits.