How we continuously validate formal specifications in production

But they remain valuable only as long as they reflect reality. At Datadog, we encountered this challenge while working on Husky, our event database. We had a formally verified model of Husky's routing system that matched production behavior when we created it.

Over time, though, Husky evolved, and a change to its placement logic allowed conflicting placements to persist in production for about a year. Although harmless during normal operation, just two conflicting placements would have caused Husky’s backfill system to crash while recovering from placement data loss. We found the issue not by triggering that failure, but by checking production behavior against our TLA+ specifications.

That raised a question: How do you know when a specification has drifted away from the system it was meant to describe? To answer that question, we built FETCh (Formal Execution Trace Checker), a system that turns TLA+ specifications into runtime monitors.