How We Continuously Validate Formal Specifications in Production
Datadog, Thursday, November 5th, 2026
Datadog built FETCh to continuously validate production behavior against TLA+ specifications, uncovering a year-old bug in Husky.
Datadog found that its Husky event database's routing system had drifted from its formally verified TLA+ model, as a placement logic change let conflicting placements persist in production for about a year.
The conflicts were harmless normally, but just two would have crashed Husky's backfill system during recovery from placement data loss.
To detect such drift, Datadog built FETCh (Formal Execution Trace Checker), which turns TLA+ specifications into runtime monitors to validate production behavior at scale.
The post explains the tension between model-checkable specifications, which need bounded inputs, and observable ones, which must handle unbounded real traffic and describe what is allowed rather than how.