Copilot
Copilot is a stream-based specification language and runtime-verification framework for hard real-time systems: specifications can be interpreted for testing or compiled into constant-memory, constant-time C99 monitors.
Copilot is a runtime verification framework for hard real-time systems. Specifications are written in a high-level, stream-based language, then either interpreted for testing and debugging or translated into C99 code that can be embedded in a project or run standalone.
The generated C99 monitors run in constant memory and constant time, which suits systems with hard real-time requirements such as embedded software. The specification language has an expressive static type system that catches errors early, theorem-proving extensions for proving properties about a specification, and support for obtaining proofs of correctness for the generated code.
Copilot is written in Haskell and installs through system package repositories on recent Debian, Ubuntu and Fedora releases, or by building from source with GHC and Cabal on other Linux distributions and macOS.