There is another way formal methods parallel documentation: both are futile unless you can prove that the modelized/documented system matches the actual, live one.

"This is just a matter of discipline" is not very convincing, especially when the discipline involves long unpaid afterhours.

The examples I've seen in this report from AWS are mostly about one-shot events (helping going through important changes). It's good to see formal methods used in these cases of course, but I'd really like to read stories about how sustained use of formal methods helps reclaiming the high costs of the initial investment as the actual system evolves alongside the modelization.