Runtime verification (RV) is a formal monitoring technique that uses formal specifications to create monitors. Stream runtime verification (SRV) extends RV from Booleans observations and verdicts to diverse data, allowing much richer monitors. This expressivity is challenging for developers of monitoring engines, so SRV tools end up fixing a collection of data theories for an application domain, and require significant overhead to incorporate new datatypes. Recent results allow incorporating Haskell datatypes transparently into generic SRV engines through the use of an embedded DSLs, but the resulting syntax is conditioned by Haskell, every new monitor requires recompilation and error reporting is cryptic.

In this paper, we introduce Mola, a generic implementation of an SRV engine that uses reflection in Haskell to implement a universal interpreter that offers data-theory extensibility and type guarantees as well as a simple syntax with useful error reports.

Mola introduces the role of data-theory engineer, who easily defines datatypes for each application domain and compiles Mola into a specialized engine. The resulting tool is then used by specification engineers who define monitors that the engine can evaluate without recompilation. Hence, Mola finally realizes the promise of SRV to provide a clean separation between datatypes and temporal engines.