Many costly bugs come not from code, but from flawed designs: a common challenge in complex high-performance systems. TLA+ lets us model designs directly, test them for errors, and fix flaws before writing code. 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.
Hillel is a formal methods consultant, the author of Learn TLA+ and Practical TLA+, and a member of the TLA+ and Alloy boards. His other work includes *The Crossover Project*, a collection of interviews with traditional-turned-software engineers, and *Let's Prove Leftpad*. In his free time, he juggles and makes chocolate. He did, in fact, bring enough for everyone.
