Formal methods are precisely for the domains where the semantics are well-defined. Logical circuits (a lot of CPU components get formal verification), kernels, protocols, parsers, compilers, cryptography, security frameworks, concurrency primitives, etc. all benefit a lot from verification.

Google's results page isn't well defined. But probably 90%+ of the code below it is well defined.

And in some cases, where the result isnt well defined, it can be learned, so it's not about sitting and thinking what would make sense.