How we use formal modeling, lightweight simulations, and chaos testing to design reliable distributed systems | Datadog

This post details the application of formal modeling (TLA+), lightweight simulations, and chaos testing to the design of Datadog's new message queuing service, Courier. It describes Courier's requirements for multi-tenancy, at-least-once delivery, graceful degradation, and horizontal scalability. The design leverages multiple FoundationDB clusters for multi-tenancy and a broker layer for API exposure. The use of TLA+ and simulations is highlighted as a method to validate system-level properties and failure modes during the design phase, complementing traditional testing methods.