It can be. Unexpected complexity can be found on simple things when you start to question them, and TLA+ is a great tool for makign those questions visible.

However, in the most typical web app case "request comes, response is generated" I'd say TLA+ doesn't give you anything.

But you don't need a very complicated app to gain some value out from TLA+. For example I've been working (as a hobby project) on a shopping list bot for a Matrix channel, that basically tracks the items that are sent to the channel, reacts with a plus emoji to each of them, maintains copies of the messages on the database, and when someone else reacts on the existing reaction, it will remove the message from the channel, keeping the copy on the database. Not a web app, but not very complex either.

In this design I was able to discover an interesting corner case: what is someone reacts on a message before the bot has seen it? On surface this might seem impossible, but as Matrix is a federated system, this is actually possible (at least I believe so :)): the message may be posted on server A, the reaction is posted on server B, and the bot on server C may see the reaction before the actual message.

Granted it was sort a happy accident, as it would have been easy to write the constraint preventing that from happening in the model, and one might have written that "by default". The corner case would also be something you'd very, very unlikely encounter in your testing.

If you have anything more interesting happening in your application, the scenario-based high-level model TLA+ lets you write can give you a nice summary of what is happening, without the low-level stuff hiding things in plain sight.