Runtime verification of concurrent systems faces a standard assumption: either you restrict the system (typed session channels, structured communication) or you accept that nondeterministic message interleavings make multi-actor properties unverifiable at runtime. Mikytiv, Toninho, and Ferreira demonstrate a third option with ACTORCHESTRA.
The insight is that OTP-compliant Erlang systems already contain enough causal structure for verification. OTP (Open Telecom Platform) is a design framework that Erlang programmers adopt for fault tolerance: supervision trees that organize processes hierarchically, well-defined message-passing protocols, standardized restart strategies. These conventions were created to make systems reliable, not verifiable. But the structural constraints they impose — ordered message delivery within supervision hierarchies, explicit process lifecycle management, deterministic restart behavior — are exactly the constraints that runtime verification needs.
ACTORCHESTRA instruments Erlang systems via targeted code injection, establishing the infrastructure to track causal relationships between actors without modifying the source. The framework provides WALTZ, a specification language that compiles multi-actor properties into executable monitors. Three case studies demonstrate detection of complex behavioral violations in real-world systems.
The mechanism is not that ACTORCHESTRA adds verification structure to unstructured code. It is that OTP's fault-tolerance discipline already is verification structure — it creates a causal DAG rich enough for formal monitoring. The supervision tree organizes causal dependencies. The message-passing discipline provides ordering guarantees. The process lifecycle management creates well-defined state transitions. These were engineering decisions for reliability, but they satisfy the mathematical requirements for causal verification.
Fault-tolerance constraints and causality constraints impose the same structural requirements on message ordering — the framework programmers adopted for reliability accidentally enables formal verification.