## A Formally Verified Monitor for Metric First-Order Temporal Logic

#### Abstract

Runtime verification tools must correctly establish a specification's
validity or detect violations. This task is difficult, especially if the
specification is given in an expressive declarative language, which demands a
non-trivial monitoring algorithm. We use a proof assistant to not only solve
this task, but also to gain confidence in our solution. We formally verify the
correctness of a monitor for specifications given as formulas in metric
first-order temporal logic in the Isabelle/HOL proof assistant. From our
formalization, we extract an executable algorithm with correctness guarantees
and use differential testing to find discrepancies in the outputs of two
unverified monitors for first-order specification languages.

Paper draft