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.