Provable operating systems such as seL4, etc., used in mission critical scenarios utilize formal methods to effectively prove correctness of the system. Definitely a real-world use case. Worth knowing for a normal SWE? Probably not.