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+.

In this guide, I want to demonstrate how to use TLA+ to specify a simple serverless system.

AWS defines serverless as:

A serverless architecture is a way to build and run applications and services without having to manage infrastructure.

You design your system as a collection of small runtime entities, often connected to queues to exchange messages.

AWS offers services like Lambda and SQS to easily provision such systems. With managed services, less development effort is required to have something up and running. Additionally, they make it easier to build scalable and resilient solutions.