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.

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.

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.