Quite a lot of things can and have been formally verified with formal methods.
1. Compilers. We want to prove that a compiler preserves the semantics of its source program. For example, if we write a int x = 3; x++; in C, we mean that. But the compiler might not produce correct assembly and machine code.
It is known to be difficult to debug compilers, so a bunch of people at INRIA, the French national lab for computer science, led by <PERSON>, decided to start from scratch and write a C compiler that is provably correct. Eventually, they produced CompCert, which has since been used commercially by companies like Airbus to compile important software.
There have also been certified compilers for other languages. One of such exists for ML (CakeML). I would not surprised to find more.
Note: According to @BasileStarynkevitch, CompCert has been used for purposes related to aviation, but it is not sure if Airbus is using it to compile on-plane software as of June 2018. According to <PERSON> (via personal communication to Basile), last year Airbus was still considering this as a possibility. But at least it has been used for something.
1. Operating system kernels. Operating system kernels are also hard to debug, and can be pretty nasty if there's a bug (it stops the entire machine!). 904
If you run into a OS kernel bug on a satellite, it wouldn't be a very good day for you. So, a bunch of researchers in Australia wrote an operational specification for an OS kernel. Then, they developed a kernel according to that specification and proved it free of bugs (e.g., deadlocks, livelocks, overflows...). Of course, the spec is assumed to be correct. That became the seL4 kernel.
For follow-up on this work, see HACMS (a project which developed a verified drone based on seL4) and CertiKOS (a project which developed a layered, POSIX, concurrent OS kernel).
1. An example closer to us. Part of the control software running on the Paris Metro Line 14 is formally verified using the B-Method. Later, the B-Method was also used on Line 1 when it was automated. The French people really like formal methods!
Of course, most software would be too costly to verify. I doubt anyone would want to fully verify a browser or a word processor, as they don't matter all that much (if they crash, just restart!). But if your software is running on an airplane or a train carrying a hundreds of people and tasked with operating the vehicle, it would be reasonable to want to verify that.
<PERSON> logic and/or operational semantics per se might not be that useful in software development, but they are important theoretical and/or intellectual foundations of useful verification methods. Therefore, they're still important to have a sound grasp and understanding of those tools. I believe it wouldn't be an exaggeration to state that every software verification expert (or quasi-expert) has a good understanding of <PERSON> logic and operational semantics! 81