TLA+ is an indispensable tool for maintaining correctness in highly complex, concurrent environments. Why isn’t it used more in industry? One of the objections levied in general at formal methods is that they require a substantial investment in time, in opposition to other software development activities. Our experience at CrowdStrike is that this simply is not true.
In this talk, I’ll review past and ongoing experiences with TLA+ at CrowdStrike. In addition to a number of smaller, targeted engagements with TLA+ in the past, the talk will highlight the outcome of a recent effort to expose colleagues to TLA+ and drive more widespread use. Over only 5 days of workshopping, the participants with minimal TLA+ expertise were able to identify multiple potential failure cases using TLA+ models.