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.

Last week, I’ve re-read “Test Driven Development: By Example” by Kent Beck. I was amazed by the simplicity of his process, consisting of small pragmatic steps. So, I decided to put the process to the test in an unfamiliar domain.

The kata

In this kata, I am going to develop a serverless service in AWS using a Lambda and the API Gateway. I chose this task because, on the one hand, it will contain a fair amount of infrastructure code, which is considered hard to test. On the other hand, because I wanted a task that was more abstract and closer to a business requirement in contrast to a technical requirement like ‘deploy an AWS HTTP API Gateway’.

CloudFormation and Terraform are both tools to describe your infrastructure as code. They enable us to easily provision, re-provision and update our infrastructure without losing control of all the changes. I’ve used both tools many times in different products, and I was never in a situation that either tools let me down. That being said both tools have strengths and weaknesses. On the one hand, Terraform configuration files tend to be more concise and readable, on the other hand CloudFormation offers better support for rotating servers. In this blog post, I am going to show you how you can use CloudFormation or Terraform for this job and what are the trade-offs of each tool.