Hello tlaplus community,
I am Georgios, I am a developer and lead consultant at Thoughtworks.
One of the new trends in the industry is building systems using a "serverless architecture".
This usually means designing systems as small Lambda functions connected with queues and API gateways that your cloud provider takes care of running for you.
The traditional testing pyramid doesn't work very well for those systems. Partially because running many of those components locally is hard or even impossible and also because those systems tend to be highly asynchronous.
I was wondering if TLA+ can have a role to play in increasing our confidence that those systems are working as expected. Is there maybe a competitive value proposition for using TLA+ specifications with serverless. Since, testing is now harder and it is already challenging to test for bugs arising from asynchronicity?
I am curious if anyone has any experience to share with using TLA+ in an agile team. Has anyone incorporated TLA+ and the act of writing specification in their team processes, and CI/CD pipeline?
Additionally, I recently wrote a blog post to demonstrate that specifying serverless systems in PlusCal is relatively easy and will catch nasty bugs.
Happy to hear your thoughts about the post too[1].
Best regards,
Georgios Chinis