How we continuously validate formal specifications in production

Datadog's engineering blog describes FETCh, a tool that turns TLA+ specifications into Rust runtime monitors fed by production telemetry, so drift between a formal model and the running system gets detected. Applied to Husky's routing, it found no violations in the router, but flagged conflicting placements that had been stored for about a year and could crash backfill recovery. Datadog reports roughly 2% CPU overhead in sidecars. These figures are self-reported, and the tool supports only a subset of TLA+.