Erla+: Translating TLA+ Models into Executable Actor-Based Implementations

Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs. In this paper, we present Erla(+), a translator which automatically translates models written in a subset of the PlusCal language to TLA(+) for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment. W e show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.