One of the arguments for formalizing it anyway is that when you inevitably make changes due to the real world, you can see exactly what else might need to change.

The same argument goes for type safety in general: would you rather "know" how it all works all the time and make the changes without assistance (ample evidence this is generally not possible beyond toy scale) and discover later what you missed, or encode expectations into types so a significant chunk of it is "chase compiler errors"?

Neither is ideal in all cases, there's plenty of room for both.