ConfPad

Distributed systems are hard. How do you test your system when it's spread across three services and four languages? Unit testing and type systems only take us so far. At some point, we need new tools. Enter TLA+. TLA+ is a specification language that describes your system and the properties you want. This makes it a fantastic complement to testing: not only can you check your code, you can check your design, too! TLA+ is especially effective for testing concurrency problems, like crashes, race conditions, and dropped messages. TLA+ is so effective for this that both AWS and Azure teams consider it essential to their work. It keeps subtle, serious bugs out of their code and helps them optimize without losing correctness. And it's not just for the cloud: engineers have used TLA+ to verify everything from business workflows to video games. This talk will introduce the ideas behind TLA+ and how it works, with a focus on practical examples and how you can apply it to your own work.