We design and implement trustworthy software tools for Erlang, by using formal methods.

Our key asset is a formal semantics for Core Erlang, mechanized in the Rocq theorem prover. Besides developing this formal foundation, our team is working on creating applications on top of the mechanized formal semantics, because we want to build formally based, high-assurance tools for the BEAM community.

A mechanized formal semantics for Core Erlang

Formal semantics describe programming languages with mathematical precision. With the semantics, one can examine program behaviour, define program equivalence, and formally verify program correctness or program safety. We defined formal semantics for Core Erlang, a standard intermediate language in Erlang/OTP; this allows us to develop high assurance tools not only for Erlang but also for other BEAM-based languages such as Elixir, Gleam and LFE.

Our mechanized formal semantics includes a fairly complete, mathematically precise definition of the behaviour of sequential and concurrent features of (Core) Erlang, including the actor model and its fault tolerance features. Furthermore, we defined program equivalence so we can mathematically prove or disprove if two programs behaviours are indistinguishable, enabling the verification of refactoring and optimisation.

Our formal definition has been validated against the reference implementation, that is, it is assured by automated testing that the behaviour we defined for programs matches their behaviour when run in the interpreter.

Technical highlights:

Security verification

The formal semantics defines every possible behaviour of programs, finite or infinite, deterministic or nondeterministic. Vulnerable behaviour can be mathematically defined, and formally verified and machine-checked in our implementation. As a first case study, our team has demonstrated proving atom exhaustion vulnerabilities by using a calculus tailored for this proof domain. We are looking forward to extend this work by formally defining security guidelines and certifying compliance, as well as formally verifying CVE affectedness (pending Horizon Europe grant application).

Property verification

We can state correctness properties about the programs and we can verify them against all possible behaviours identified by the semantics. Work-in-progress in this topic is demonstrated by automatically proving basic properties of integer-processing recursive functions and list-processing recursive functions. These prototypes formalise Hoare-triples that were manually constructed from QuickCheck properties, but automatic translation for these is a straightforward, technical step. The development of these was supported by the EEF Stipend program.

Note that as far as we understand, our method for property verification is fundamentally different from the approach used in Lynx. Although both are based on the idea of turning contracts and program properties into proof obligations, Lynx translates Elixir programs into Lean by using a shallow embedding of functions (Elixir functions become Lean functions and their behaviour is defined by host language semantics). That is, this approach incorporates unverified, trusted code base (which brings programs and their specifications into the verification tool), and necessitates further (nontrivial) validation of whether the property proved formally is reflected in the program’s actual behaviour. In contrast, our approach uses deep embedding and defines the behaviour explicitly over the abstract syntax deeply embedded in the theorem prover. Thus, programs can be processed by the semantics without translation, but by a trivial mapping from the abstract format to the abstract syntax used in the theorem prover. This allows us to bring programs into the verification pipeline effortlessly and safely.

Certified compilation

Our team carries out a 4-year (2026-2029) project that develops a certified optimising compiler for Core Erlang. We will implement a compilation from Core Erlang to BEAM via ANF and SSA, and will implement and verify many of the standard optimisation steps also available in the Erlang/OTP compiler. Currently, the intermediate languages are under development, investigating a common language metatheory that facilities the verification of translation and optimisation steps.

Featured publications

Contact