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.
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.