Yeah, there's got to be some sweet spot between "formally verify all the things" and "i guess this diff looks okay, yolo!".

I'd say that if you're designing a system which has the potential to disconnect half your customers based on a misconfiguration, then you should spend at least an hour thinking about what sorts of misconfigurations are possible, and how you could prevent or mitigate them.

The cost-benefit analysis of "how likely is it such a mistake would get to production (and what would that cost us)?" vs "how much effort would it take to write and maintain a verifier that prevents this mistake?" should then be fairly easy to estimate with sufficient accuracy.