Has anything actually useful ever come out of this field of enquiry? To me it always seems like excessive formalism for its own sake without a useful real-world outcome. Would be happy to be wrong about this.
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.
The burden of using these extreme approaches is high, but there are definitely circumstances where it is warranted. Think of it as TDD on steroids.
The CompCert C compiler: https://compcert.org/
TLS implementation in Firefox: https://blog.mozilla.org/security/2020/07/06/performance-imp...
Elasticsearch model checks some of their core algorithms with TLA+: https://youtu.be/qYDcbcOVurc.
Amazon is known to apply formal methods in varying forms to services like S3: https://www.amazon.science/publications/using-lightweight-fo...
Many components in airplane software is formally verified in some aspect.
Formal verification has it's success stories, like seL4 (https://sel4.systems/).
This series seems rather educational and seems to give you coq proofs for algorithms. I guess it depends on your needs and domain if you need to bother.
AWS build some of it's services with their help.