eSpark used TLA+ to prove no design met all 3 rules, then traded one away

eSpark Learning, an ed-tech provider for primary schools, ran a manual, semi-regular configuration process for every customer that coordinated several third-party systems and directly modified customers' IT networks. As the user base grew, the workload became unsustainable — the support team realized it would need a new full-time hire every year just to keep up. Leadership had always judged automating the process too dangerous: a mistake could touch a customer's network and cost the contract.

Engineer Hillel Wayne had recently used formal specification (in the TLA+ style) on a batch-uploader project and shaved a week off delivery by catching architecture bugs before writing code. The project manager had defined three properties the automated replacement had to guarantee to be safe. Wayne modeled the system in a specification language and ran it through a model checker, which exhaustively simulates every scenario a spec allows and returns a concrete trace when it finds one that breaks a rule.

After two days of modeling, every design either broke immediately or contained a subtle flaw that could sit unnoticed in production for months before collapsing. Some designs satisfied two of the three required properties, but none satisfied all three. Instead of picking one anyway and hoping, Wayne brought the project manager into the modeling artifacts, showed concretely how each design would fail, and asked which property the business could live without.

In-house design experts determined one property only needed to hold usually, not always. With that single trade narrowed, the model checker confirmed several designs would now work, and the team built one of them. The automated configuration service ran without incident for years afterward, outlasting the tenure of the engineers who built it.

Model checker proved no design met all 3 rules; negotiate

Modeling in a specification language is cheap to throw away; a mostly-built codebase is not, so testing every design idea before implementation avoided wasted engineering time.

A model checker returns a concrete failure trace, which is more persuasive to a non-engineer stakeholder than an abstract risk warning.

Surfacing 'none of these designs satisfy all three requirements' before writing code turned an implicit, unexamined assumption into an explicit decision the project manager could actually make.

When every design you try seems to fail, model the space formally first. A model checker turns a vague sense of risk into a specific, negotiable trade-off you can raise before any code is written.

The automated configuration management service ran efficiently for years, well beyond the tenures of the engineers who built it. Wayne went on to work full-time as a formal specification consultant and write about the practice, including a book on the subject and documentation work for the Alloy specification language.