BeepBeep3
A free, open-source Java stream-processing engine (under 250 KB, no external dependencies, LGPL) for analyzing log data and live event feeds. Uses a pipe-and-processor architecture where small "processors" are connected into chains that transform events in real time; chains can be auto-rendered graphically. Supports network packet analysis and data mining via dozens of extensions.
Breach
Breach is a MATLAB toolbox for simulation-based analysis of dynamical, cyber-physical, and hybrid systems. Properties are written in Signal Temporal Logic (STL) and evaluated using quantitative (robustness) semantics rather than plain Boolean verdicts, so results indicate not just whether a specification holds but by how robust a margin. It integrates with Simulink for running and analyzing parameterized simulation campaigns, and supports falsification — using optimization to search for parameter values that violate a requirement.
Daut
Daut is an internal shallow DSL, effectively a library, in the Scala programming language for programming monitors. A specific monitor is defined as a subclass of a library Monitor class. Given an object a monitor, one can submit events to it. Events can be any Scala data object respecting the parametric event type of the monitor. The body of the monitor is written in a combination of rule-based programming and state machines, with the additional feature that event sequences can be specified without having to name intermediate states. The DSL relies heavily on the use of Scala's elegant pattern matching to match against events. The internals of Daut are fundamentally a rule-based paradigm, where the state of a monitor at any time is a set of active facts, where a fact is an object parameterized with data. However, a fact has transitions leading to new facts. For each event submitted to a monitor, the relevant active states are applied to the event, causing facts to be removed and/or added. Due to the existence of transitions in facts, they can also be perceived as states in a state machine, but where states carry data in contrast to classical state machines, leading to a more powerful paradigm. Monitors can be chained together such that one monitor can deliver events to other monitors. Since Daut is an internal DSL, rules/state machines can be combined with code, allowing to generate data in addition to just Boolean verdicts.
DejaVu
DejaVu is a Scala-based runtime verification tool that checks event logs against specifications written in first-order past-time linear temporal logic, extended with recursive rules and quantification over observed data. A specification compiles to a synthesized Scala monitor program, which is then run against CSV-formatted (optionally timestamped) event logs; internally it uses Binary Decision Diagrams to represent assignments to quantified variables efficiently. Output includes violation reports, event statistics, and timing metrics.
DetectEr
detectEr monitors asynchronous component systems running on the Erlang VM for conformance to correctness properties written in sHML, a runtime-monitorable fragment of the modal mu-calculus. Specifications are compiled into Erlang monitoring code that can be woven into a system inline (static instrumentation), outline (dynamic instrumentation via Erlang's tracing infrastructure, treating the system as a black box), or offline (replaying recorded trace events).
JavaMOP
Implements Monitoring-Oriented Programming (MOP), integrating formal specifications with Java code for runtime verification. Uses AspectJ instrumentation to auto-synthesize monitors from specified properties and weave them into the running system; monitors trigger user-defined actions (logging, recovery, etc.) on violation or validation. MIT-licensed, maintained by the Runtime Verification organization.
JunitRV
jUnitRV is a runtime verification framework that integrates seamlessly with the JUnit testing infrastructure for Java, enabling property-based monitoring during unit test execution. It allows developers to specify temporal properties in a high-level specification language, especially LTL, and automatically generates monitors that check these properties at runtime. jUnitRV is particularly useful for augmenting traditional testing with formal temporal specification checking. In other words, it offers checking temporal assertions rather than only assertions alone. By embedding monitors into test cases, it supports identifying bugs related to sequences of method calls, object states, or temporal constraints. Its integration with JUnit makes it accessible in standard Java testing workflows.
LogFire
LogFire is a Scala DSL (API) for rule-based programming, designed for monitoring event streams such as log files. It implements a variation of the RETE pattern-matching algorithm adapted for events — facts with limited lifespans — rather than the static fact bases RETE is normally used for, letting rules be written directly within ordinary Scala programs.
MSTLO
mstlo (mistletoe) is a Rust library for online monitoring of Signal Temporal Logic (STL) specifications. It is designed for high performance and low memory usage, making it suitable for real-time monitoring of Cyber-Physical Systems. Python bindings are published as mstlo-python.
MarQ
MarQ implements Quantified Event Automata (QEA), a specification formalism for runtime monitoring, in Java. Specifications are built programmatically via QEABuilder (states, transitions, events, quantification, guards) and monitored either offline against recorded CSV/XML trace files or online against a live system using AspectJ bytecode instrumentation; violation handling supports configurable restart (REMOVE/ROLLBACK/IGNORE) and garbage-collection (LAZY/EAGER/UNSAFE_LAZY) strategies. It extends Giles Reger's PhD research on runtime monitoring.
MonPoly
A prototype offline monitoring tool from ETH Zurich that checks compliance of log files against policies written in Metric First-Order Temporal Logic (MFOTL). Takes a signature file (relation/parameter types), a formula file (the MFOTL policy), and a log file (timestamped tuples), then reports violations/satisfactions with timestamps and data values. Used for auditing, compliance checking, and usage-control enforcement.
Montre
Montre is a timed regular expression matcher for searching behavioral sequences where timing relationships matter. It extends standard regular expression syntax with temporal constraints (e.g. bounding how much time an occurrence may span), and supports concatenation, union, intersection, and repetition of timed patterns. It can match offline over a whole trace or incrementally online, and is implemented in the Pure functional language.
PollyRV
PollyRV is a parametrised, event-based runtime verification tool supporting monitoring of real-time specifications, developed at the University of Malta as the second generation of the Larva tool. It establishes a clear system-monitor boundary so the monitor is technology-agnostic, splitting into a frontend (event extraction/system interaction) and a verification backend.
PyContract
PyContract is an internal Python DSL (Python 3.10+) for writing event stream monitors as extended finite state machines, where states can be parameterized with data and a "state vector" of active states grows or shrinks as events are consumed. Monitors are defined as classes extending Monitor, using Python's match/case pattern matching for transitions; events are fed one at a time via eval(event), and calling end() checks that no obligations remain outstanding. State composition operators (|, &, >>) and state types like HotState/AlwaysState let multiple concurrent scenarios be tracked without explicit state explosion.
PyDejaVu
PyDejaVu is a Python wrapper around DejaVu that splits monitoring into two phases: an operational phase in Python, where @event("name") handlers do arbitrary computation (arithmetic, string handling, state bookkeeping) on incoming events, and a declarative phase where the resulting events are checked against a DejaVu specification in quantified temporal logic (QTL). Specifications compile to Scala-based monitors via PyJNI, so it requires a Java/Scala runtime alongside Python.
R2U2
RML
RML is a system-agnostic domain-specific language for runtime monitoring and verification, developed by Ancona, Franceschini, Ferrando, and Mascardi at DIBRIS. It strictly separates the instrumentation layer (which observes events and encodes them as JSON) from the monitor. Specifications are compiled to Prolog via an ANTLR/Java/Kotlin compiler, and traces are verified by a monitor implemented in SWI-Prolog.
ROSRV
ROSRV is a runtime verification framework for the Robot Operating System (ROS) that monitors safety properties and enforces security policies by intercepting and analyzing ROS messages. It validates runtime behavior against user-defined specifications and can enforce access-control policies, integrating with ROS deployments without major architectural changes. Formal specifications can be compiled into monitors via the companion tool ROSMOP.
RTAMT
A Python 3 library for monitoring Signal Temporal Logic (STL) specifications. Supports both offline (batch) and online (incremental) monitoring; online monitoring is restricted to the bounded-future STL fragment. Includes discrete-time and dense-time monitoring classes, with an optimized C++ backend for the discrete-time case. Produces quantitative robustness degrees rather than simple true/false verdicts.
RTAMT-CPP
A C++ library for online monitoring of bounded-future Signal Temporal Logic (STL), computing quantitative robustness values rather than booleans. Processes timestamped input samples sequentially with tolerance for imperfect sampling intervals, and supports multiple robustness semantics (standard, input/output-robustness, input/output-vacuity). Unbounded future operators are only allowed at the specification's top level.
SMEDL
SMEDL (Scalable Monitoring with EDL) is a runtime verification framework where monitors are specified using an EFSM-style (extended finite state machine) formalism in .smedl files, with .a4smedl architecture files describing how monitors connect within a system. Its mgen code generator (written in Python, using TatSu for parsing and Jinja2 for templating) compiles these specifications into C99 monitoring code, which can communicate asynchronously via RabbitMQ or ROS topics for centralized or distributed deployments.
TeSSLa
TeSSLa (Temporal Stream-based Specification Language) is a runtime verification framework designed for specifying and monitoring properties of real-time and cyber-physical systems. It operates on time-stamped event streams, allowing users to define formal specifications that capture both logical and temporal aspects of system behavior. TeSSLa excels in handling sparse and asynchronous streams, and it provides native support for timing constructs such as delays, timestamps, and temporal relations. Its language includes features like stream merging, recursion, and time-based operators. TeSSLa specifications are compiled into efficient monitors for deployment in resource-constrained environments. While hLola and hStriver embed their specification languages in Haskell, TeSSLa uses its own syntax and semantics. Notably, hStriver introduces real-time as a first-class concept, similar in spirit to TeSSLa, but within a functional programming context. In contrast, hLola treats time as a data value, offering more flexibility but less direct support for real-time constraints.
TraceContract
TraceContract is a Scala-internal DSL for analyzing event traces, such as log files from running programs, against behavioral properties. It combines data-parameterized state machines with temporal logic operators in a single specification style, relying on Scala's object-oriented and functional features (partial functions, pattern matching) to host the DSL without a separate specification language.
hLola
HLola is a Stream Runtime Verification (SRV) tool that builds on LOLA, the pioneering approach in SRV, and extends it by incorporating features from the functional programming language Haskell. This design cleanly separates data computation from temporal aspects, enabling a flexible and extensible language for runtime monitoring. Stream Runtime Verification views runtime verification as stream transformation, where streams of events generated during system execution are processed into output streams to evaluate compliance with specified properties. HLola offers a domain-specific language (DSL) embedded in Haskell, allowing for seamless integration with host language constructs. As a result, it benefits from Haskell's expressive type system for event data and verdicts, functional abstraction for parameterization, access to rich libraries, support for higher-order specification transformations, and familiar syntactic elements like 'let'/'where' clauses, 'do' notation, and type annotations. It is also backed by a robust compiler targeting multiple platforms.
hStriver
hStriver is a Stream Runtime Verification (SRV) tool that builds on LOLA, the pioneering approach in SRV, and extends it by incorporating features from the functional programming language Haskell. This design cleanly separates data computation from temporal aspects, enabling a flexible and extensible language for runtime monitoring. hStriver offers a domain-specific language (DSL) embedded in Haskell, allowing for seamless integration with host language constructs. As a result, it benefits from Haskell's expressive type system for event data and verdicts, functional abstraction for parameterization, access to rich libraries, support for higher-order specification transformations, and familiar syntactic elements like let/where clauses, do notation, and type annotations. It is also backed by a robust compiler targeting multiple platforms. The main difference between hLola and hStriver is that hStriver supports real-time as a first-class citizen, whereas in hLola, time may only appear as a data value.
nfer
The nfer tool implements the eponymous language in C, with programmer interfaces in C, Python, and R. Visualization is provided via the Python interface. Nfer rules are written in an external DSL. The nfer language is somewhat unique in that it is a rule-based language for describing the state relationships of events with data. Nfer operates on labeled, temporal intervals with data where an event is considered an interval with zero duration. Rules describe the temporal and data relationships between existing intervals and produce new intervals when their conditions are met. Operations on numeric data are arbitrary, but the string operations are limited to equality matching. Nfer evaluation is undecidable in the general case, but there are known, useful fragments with evaluation complexity in PTime. The tool supports constructing C-language monitors with static memory allocation designed for embedded systems. The Python and R implementations use the C interpreter as a back-end.
rtLola
RTLola (Real-Time Lola) is an extension of the original LOLA stream-based runtime verification framework, designed specifically to support real-time monitoring. Like LOLA, RTLola uses stream-based specifications to define monitors over sequences of events, but it enhances the model by introducing explicit real-time semantics. RTLola allows users to define input, output, and parameterized streams, with powerful features such as sliding windows, aggregation over time intervals, and real-time constraints. These features enable the specification of complex temporal properties, including frequency-based or time-bounded conditions, which are common in embedded and cyber-physical systems. Compared to tools like hLola and TeSSLa, RTLola provides a clean separation between logical time and real time, allowing precise control over how temporal conditions are evaluated. While hLola focuses on leveraging Haskell's functional features and treats time as a data value, and TeSSLa integrates time deeply into its stream model with support for sparse streams and delays, RTLola strikes a balance by supporting high-level real-time constructs in a dedicated DSL with formal semantics and analyzable resource usage.