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.