I’ve used TLA+ to model a deployment pipeline. It helped to demonstrate the safety property we needed that process to maintain.
The code running the deploy process is messy and complex. But the a spec doesn’t have to be. You can represent as much or as little detail as you need.
Cool! And you make a good point: just because the actual software has 100 corner cases, doesn't mean the model has to. It can still be useful even if it just models an interesting part of the problem.
With one client I have, we know the TLA+ model is accurate because we're extracting tests directly from the spec. It's kind of a riff on what MongoDB does in this paper: https://arxiv.org/abs/2006.00915
The code running the deploy process is messy and complex. But the a spec doesn’t have to be. You can represent as much or as little detail as you need.