Most software flaws have one of two causes.

Sometimes the cause is that the code does not match the developer's design. Other times, the code correctly implements a bad design: there is a fundamental error in the model of the system. These kinds of errors are often only apparent after we fully implemented the system, which makes fixing them a costly and difficult endeavor. This is especially a problem with high-performance systems, which push us towards complex designs.

With TLA+, we can directly test our designs for bugs. TLA+ is a "formal specification language", where we can encode high-level models of software systems and then analyze their behavior. TLA+ has successfully found bugs in everything from cloud services and message queues to video games and SSD firmware. After fixing the designs, developers can implement their software with more confidence and spend less time on long-term maintenance.

This session will provide a brief overview of how and why TLA+ works, and how it can be applied to find design bugs in low-latency systems.