Some transportation systems are formally verified. I don't think anyone riding them except for extreme nerds would even know. A big part of engineering is, afte

Some transportation systems are formally verified. I don't think anyone riding them except for extreme nerds would even know. A big part of engineering is, after all, preventing harm to the public through its works. All we can prove is that some property holds. I think the major benefit is that it helps humans think about those properties and what is important. Especially in the world of computer systems it is impractical to expect a human to glance at a few thousands lines of code and spot where the race condition is. But if we simplify the model and check it with a computer it can usually find it rather fast. Formal methods don't make systems inherently safer or fool-proof but they help us think about and understand complex systems. The name of the game after all is to not fool ourselves. The challenge is that we are the easiest ones to fool (paraphrasing Feynman here).