You might create a TLA model during the initial specification process to assist you in thinking through your problem. You would then update the model going forward as your understanding of the domain improved and as system requirements changed. However, you could write a specification for an existing system as well. Any processing where the complexity seems greater than ones reasoning ability or that needs assurance guarantees, could signal the need for a high level description to guide engineering efforts.

An initial model might take 4 hours to put in place. The time would be spent thinking through how best to abstract the modeled process and its logical properties, slowly building up a more and more complete set of events, and checking the model by running it as one goes. With an initial model, additional hours would probably be spent here and there adding enhancements and finding ways to do things better, just like one would do with regular code. The model would effectively exist over the lifetime of a corresponding code artifact and guide work on the artifact.

For a standard web application that mostly does reads and writes to a database, there usually wouldn't be any need for a tool like TLA to help you reason. A general use case for TLA is describing systems where there are multiple processes or threads coordinating on some sort of shared state.There would be indeterminacy in the order in which events happen. There could be the possibility of failure and the need to handle it gracefully.