Datadog builds FETCh to validate TLA+ specs

Datadog engineers built FETCh, a system that translates TLA+ formal specifications into Rust-based runtime monitors to continuously validate production behavior at scale. When deployed to monitor Husky, the company's event database routing system, FETCh successfully detected conflicting placement logic that could have caused data recovery failures, an issue conventional testing had missed. Open article →