Past Meetup

Meetup : TLA+ - a specification language for concurrent and distributed systems

This Meetup is past

11 people went


This is the second meetup of Papers we Love Utrecht.

Behrooz Nobakht from HERE ( will give us a 30 minute presentation about TLA+, a specification language for concurrent and distributed systems. He will give an introduction to textbook examples of TLA+ and, if time allows, he will also show us real-world TLA+ specifications (e.g. the one for the raft consenus protocol).

We think it sounds very exciting and fits well with the last meetup's subject!

Links about the subject for ones who want to come prepared:

- Resources from!forum/tlaplus
- TLA+ spec for Raft at

A primer on TLA+ and its applications

We have a fast deep dive into Temporal Logic of Actions (TLA) and its associated tools (TLA+). TLA+helps to formally specify systems with simple mathematics, then verify certain properties and provehow they work. We go through an example to start using TLA+ including a specification and using the model checker. We try to provide examples on how/why using TLA+ is crucial in many softwareengineering domains. We will have an open discussion on how using TLA+ could fill the gaps indaily software engineering challenges. If time allows, we look at the TLA+ spec of a well-knowndistributed systems algorithm.
You can find the slides and resources for this talk on GitHub's repo for PwL Utrecht after thetalk.

I am Behrooz, a software engineer with a specific focus and interest on JVM stack and programminglanguages. Since 2009, I've turned more to distributed systems and concurrency in programminglanguages to apply the principles to the practice of software engineering. I am usually active onTwitter @behruz and code on GitHub @nobeh.


Speaker, food and drinks have all been provided by the lovely people at HERE. If you're into cartography and/or computer science, you should definitely check them out.


19:00 Welcome + Food & Drinks
19:30 Talk + Discussion
20:15 Drinks & Social
21:00 Fin

General information

This meetup is the second in a series about distributed systems. Possible future topics are:
* Dynamo: Amazon’s Highly Available Key-value Store (
* The Raft consensus algorithm (
* SQL isolation levels (

We are also interested in other topics of course. Or new series. If you want certain topics to be covered or want to present a topic yourself, don't hesitate to contact us!

Finding the place

We are hosted at the Marinus Ruppertgebouw on De Uithof. It's easily reachable by car or public transport. For public transport, bus 12, 27, 28 and 128 run regularly. Get off at "Heidelberglaan" and cross the street. It's the building behind the green flat.

If you are coming by car, follow the "De Uithof" signs if you're on Utrecht's ring road.

The room is located on the first floor of the Marinus Ruppertgebouw. We will get some signs up to guide you there. Also, a map of the building can be found here:


There are many (paid, but not that expensive) parking spots around the campus. Behind the Marinus Ruppertgebouw, there are some free parking spots but they are usually occupied. It's worth a shot though