Erlang is a language with built-in support for concurrency and distribution. Thanks to its high abstraction level, concurrent systems that utilize multiple nodes can easily be built. Reasoning about the correctness of concurrent Erlang systems is a difficult task, but tools exist that can help. When distribution enters the picture however, reasoning becomes overwhelmingly complex and there are no tools that can come to the rescue.

This paper was motivated by a challenge we faced while re-architecting a critical component in Klarna’s software stack. We wanted to reason about correctness aspects of a new distributed algorithms, developed for use at the very core of Klarna’s business. We tackled this challenge by designing and developing a general model of the behaviour of distributed Erlang nodes, that is however executable in a single Erlang node. We present our distributed Erlang model and demonstrate its capabilities in our case study, showing how it was used to model and test the new distributed algorithms with the help of Concuerror.