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.