Let's be honest: writing correct concurrent and distributed code is hard. Race conditions? Deadlocks? They're the bane of modern software development, especially with tools like Kafka, Kubernetes, and microservices. Testing helps, but it rarely finds all the subtle, timing-dependent bugs.

Imagine having a way to mathematically verify your design's logic before you code it. That's TLA+. Developed by Turing Award winner Leslie Lamport, it's a language for specifying and checking algorithms, especially concurrent ones. The catch? Most intros are dense and theoretical.

This session is different. It's TLA+ for the rest of us – the software engineers in the trenches. We'll skip the deep math and focus on practical application. You'll learn what TLA+ is, how to model simple concurrent interactions, and how it can save you from deployment disasters by catching design flaws early. Walk away ready to explore how formal methods can become your secret weapon for building bulletproof systems.

Key Takeaways:

• Recognize the inherent difficulties in validating concurrent designs.
• Get a practical, hands-on feel for TLA+ concepts and syntax.
• Understand how TLA+ helps prevent race conditions and deadlocks at the design stage.
• Be inspired to apply formal verification techniques to real-world problems.

Consulting software architect / lead dev. Specialized in backend performance optimization. Wrote THE French book on Go: https://osinet.fr/go/en/ - Main non-tech business interests: media and e-commerce.

Also, playing bass guitar with lots of distortion when I get the chance.