In large organizations, authorization can be a very complex topic. Almost always it is tightly constraint with strict compliance requirements, while at the same time it is intricately tied to the user experience. Who hasn’t had the experience of trying to access a resource they need for work only to be stumped by insufficient access, access that can sometimes take days or even weeks to be granted.

For engineering platform teams, that is an especially acute problem. As it is part of their mission, to provide a seamless experience and at the same time they need care for authorization of multiple offerings that multiples the pain of any friction.

How should two microservices communicate?

Let’s analyze two different communication patterns:

• Polling: Service B periodically query Service A for the current state of the users and updates its local storage.
• Event driven: Service A publishes in a queue every time user information is updated. Service B consumes the updates to stay up to date.

Using TLA+ we are going to model the two different patterns to see how well they fit our requirements. In our specification, we are also going to take into account unexpected failures that can affect the system and show how to model them in TLA+.