While serverless platforms substantially simplify the provisioning, configuration, and management of cloud applications, implementing correct services on top of these platforms can present significant challenges to programmers.
For example, serverless infrastructures introduce a host of failure modes that are not present in traditional deployments.
Individual serverless instances can fail while others continue to make progress, correct but slow instances can be killed by the cloud provider as part of resource management, and providers will often respond to such failures by re-executing requests.
For functions with side-effects, these scenarios can create behaviors that are not observable in serverful deployments.

In this paper, we propose mu2sls, a framework for implementing microservice applications on serverless using standard Python code with two extra primitives: transactions and asynchronous calls.
Our framework orchestrates user-written services to address several challenges,
such as failures and re-executions,
and provides formal guarantees that the generated serverless implementations are correct.
To that end, we present a novel service specification abstraction and formalization of serverless implementations that facilitate reasoning about the correctness of a given application's serverless implementation.
This formalization forms the basis of the mu2sls prototype, which we then use to develop a few real-world microservice applications and show that the performance of the generated serverless implementations achieves significant scalability (3-5$\times$ the throughput of a sequential implementation) while providing correctness guarantees in the context of faults, re-execution, and concurrency.