> Some may argue that there's no guarantee that such proofs apply to real world systems.

I would argue that those who would argue that have probably not spent a lot of time doing any real-world formal verification.

People seem to like arguing about its utility in the abstract without ever doing it.