In many fields the gains are not worth the effort if you think of validating entire specs or real codebases.

Yet TLA+ can be beneficial to validate multiple-step interactions between components e.g. a quorum protocol on a network or locking and messaging between threads. Anything that involves more than one agent and a state machine essentially.