Apart from the intellectual clarity, you don't need to employ all of the tools in this text to benefit practically from some use of formal verification, etc. If you're using a statically typed language, you're likely already benefiting from at least some degree of verification. Your types encode your specification.

One example close to home for me and from industry is a dependently typed language we are working on at my company that's used to encode validations and transformations for transaction reporting (other teams have also begun to use the language for other uses). Consistency is ensured by the type checker and the compiler subsequently generates the aforementioned transformation and validation functions that are used in production. This is admittedly a very niche application, but as I've already written, the use of static analysis admits a range of rigor—it's not either/or—so it's a question of determining the appropriate degree of formality for your particular case.