Verifying Actor Systems: Beyond Testing
Actor systems are notoriously difficult to verify through traditional testing. Message ordering is non-deterministic, properties often span multiple actors, and a protocol violation that only manifests under a specific interleaving can hide in production for months.
The 2025–2026 literature offers three complementary answers to this problem, each attacking a different layer of the verification stack: runtime verification of causal properties, formal deadlock detection from the outside, and static protocol typing at compile time. Together, they sketch a path from “we tested it and it seemed fine” to “we have evidence that it is correct.”
This article breaks down all three — and connects them back to the pedagogical argument that Erlang’s supervision model is not a set of APIs to memorize, but a set of contracts to understand.
Why testing actor systems is not enough
A unit test checks one process in isolation. An integration test checks a few processes under a specific schedule. But an actor system’s behaviour depends on which messages arrive in which order — and the number of possible interleavings grows combinatorially with the number of actors.
Worse, the properties we actually care about are often cross-actor:
- “Whenever the order actor confirms a purchase, the inventory actor must have received a reservation first.”
- “If a service sends a request, it eventually receives a response — or is provably deadlocked.”
- “No process ever sends a message that violates its declared protocol.”
None of these can be verified by testing a single process. They require either observing the running system or proving properties before it runs.
The three approaches below take one of those two paths.
1. Runtime verification: ACTORCHESTRA and WALTZ
ACTORCHESTRA is a runtime verification framework for Erlang that automatically tracks causality across multi-actor interactions. It was presented at the 2026 IEEE International Conference on Software Testing, Verification and Validation (ICST) in the paper “In Perfect Harmony: Orchestrating Causality in Actor-Based Systems.”
The core problem it solves is stated precisely in the abstract: “Properties frequently span multiple actors with complex causal dependencies, while non-deterministic message interleavings can obscure execution semantics. Moreover, most existing monitoring tools are designed for single-process behavior.”
ACTORCHESTRA addresses this in two parts:
- Targeted code injection into Erlang systems that follow OTP guidelines — establishing the orchestration infrastructure needed to track causal relationships without manual modification of the target system.
- WALTZ, a specification language that compiles multi-actor properties into executable Erlang monitors that integrate with the instrumented system.
A concrete property you can express in WALTZ:
“Whenever the order actor sends a confirmation message to the customer actor, the inventory actor must have received a reservation message beforehand.”
This is a causal chain — not a simple state predicate. ACTORCHESTRA monitors the chain at runtime and alerts when the property is violated. Three case studies demonstrate its effectiveness in detecting complex behavioural violations in real-world actor systems.
The trade-off is explicit: the paper quantifies the runtime overhead of the monitoring infrastructure and analyses the balance between added safety guarantees and execution costs. Runtime verification is not free — but it catches violations that no unit test would ever see.
2. Formal deadlock detection: DDMon
DDMon (2025, OOPSLA) takes a different tack: instead of instrumenting the system’s source code, it deploys distributed black-box monitors alongside each service and detects deadlocks by only observing incoming and outgoing messages, exchanging probes with other monitors.
The formal contribution is significant:
- A formal model that captures RPC-based application styles — including
gen_serverprocesses in Erlang/OTP. - A distributed black-box monitoring algorithm proven sound (no false positives) and complete (no false negatives).
- A Coq mechanisation of the results.
This is the first work that formalises, proves the correctness of, and implements distributed black-box monitors for deadlock detection.
The DDMon tool implements these monitors for Erlang and Elixir applications based on gen_server, with minimal user intervention. It also optionally collects logs via the Erlang/OTP trace mechanism and visualises them to help diagnose deadlocks.
Why black-box matters: the monitoring does not depend on the internal syntax of the services — the process internals are not observable by the monitors. You can attach DDMon to a running system without modifying it, and trust its verdict because the algorithm was proven correct.
For practitioners, the message is direct: if you have gen_server processes making chained synchronous calls — a common microservices pattern — DDMon can tell you when they are deadlocked, and its answer is mathematically guaranteed.
3. Static protocol typing: NVLang
Both ACTORCHESTRA and DDMon operate on a running system. NVLang moves the verification to compile time.
Erlang has no static guarantees about message protocols. Processes communicate by sending arbitrary messages that are filtered by pattern matching at runtime — which means protocol violations are deferred to production failures.
NVLang is a statically typed functional language that compiles to Core Erlang, preserving interoperability with the existing ecosystem. Its central contribution is that algebraic data types (ADTs) naturally encode actor protocols: each actor declares the sum type representing its message vocabulary, and the type system enforces protocol conformance at compile time.
Two further constructs complete the picture:
-
Typed process identifiers (
Pid[T]) encode the protocol an actor expects. -
Typed futures (
Future[T]) provide type-safe request-reply patterns.
By extending Hindley–Milner type inference to track message protocols, NVLang eliminates an entire class of message-passing errors while keeping syntax clean. The type system is formalised with proof sketches for type soundness, demonstrating that well-typed NVLang programs cannot send messages that violate actor protocols.
NVLang is a separate language, but its concepts discipline pure Erlang design. Before implementing a gen_server, define the sum type of messages it accepts. That single act of specification reduces the class of errors that would otherwise only manifest in production.
How the three fit together
The three approaches are not competitors. They occupy different points in the verification timeline:
| Approach | When it runs | What it catches | What it costs |
|---|---|---|---|
| NVLang | Compile time | Protocol violations, malformed messages | Requires writing in a new language (or disciplining design) |
| ACTORCHESTRA | Runtime | Cross-actor causal violations | Monitoring overhead |
| DDMon | Runtime | Distributed deadlocks | Probe exchange overhead |
A mature verification strategy uses all three:
- Before deployment, use static typing (or its design discipline) to eliminate protocol-level bugs.
- At runtime, use ACTORCHESTRA to monitor causal properties that no type can express.
- Continuously, use DDMon to detect deadlocks that emerge from the interaction of otherwise-correct services.
The academic connection: verification as the end of a pedagogical arc
This literature connects directly to Staroletov’s 2026 Erlang Workshop paper, “Modern Erlang Teaching from Code Refactoring to Actor System Verification.” The course it describes moves students from refactoring imperative code, through Taylor-series recursion, to lightweight processes, and finally to verification of actor systems with Promela/SPIN.
The progression matters. Verification is not taught as an isolated topic — it is the culmination of learning to reason about concurrent behaviour. Students who have refactored away imperative sequencing, internalised pattern matching as type-driven dispatch, and built systems with supervision trees are ready to ask: “How do I know this is correct?”
ACTORCHESTRA, DDMon, and NVLang are three answers to that question. Each makes a different trade-off between when verification happens and what it guarantees. Staroletov’s pedagogical point — that Erlang’s model is a set of contracts to understand, not APIs to memorize — applies equally to verification: the goal is not to run a tool, but to know what property you are checking and why.
Conclusion: from “it seems fine” to “we have evidence”
Actor systems are too concurrent and too non-deterministic to verify by testing alone. The 2025–2026 literature offers a layered answer:
- NVLang proves protocol correctness at compile time.
- ACTORCHESTRA monitors causal properties across actors at runtime.
- DDMon proves deadlock freedom from the outside, with soundness and completeness guarantees.
Together, they move the field from “we tested it and it seemed fine” to “we have evidence that it is correct.”
For anyone building or teaching actor systems, the lesson is clear: verification is not a luxury bolted on after the system works. It is the final stage of learning to reason about concurrency — and the tools now exist to make it practical.
References:
- ACTORCHESTRA / WALTZ: “In Perfect Harmony: Orchestrating Causality in Actor-Based Systems.” IEEE ICST 2026. IEEE Xplore
- DDMon: Rowicki, Francalanza, Scalas. “Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation.” PACMPL (OOPSLA 2025). DOI: 10.1145/3763069
- NVLang: Guerreiro et al. “NVLang: Unified Static Typing for Actor-Based Concurrency on the BEAM.” arXiv:2512.05224, Dec 2025. arXiv
- Pedagogical context: Staroletov, Sergey. “Modern Erlang Teaching from Code Refactoring to Actor System Verification.” Erlang Workshop 2026. DOI: 10.1145/3830434.3830946
Have you used runtime verification, deadlock monitoring, or static typing in a production actor system? What did it actually catch — and what did it miss? Let me know in the comments.
Top comments (0)