Practical Insights from Datadog’s Use of TLA+ and Simulations