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