ogma: generating runtime monitors for flight and robotics software

A code generator sitting on top of Copilot

Ogma is a tool to facilitate the integration of safe runtime monitors into other systems, and the second sentence explains the whole architecture. Ogma extends Copilot, a high-level runtime verification framework that generates hard real-time C99 code.

That relationship is the thing to understand before anything else. Copilot is a specification language and toolchain in which you write properties over program state and get generated hard real-time C99 out of them. On its own that generated code is a monitor that runs somewhere and checks the property. Ogma's job is the part that is usually left as an exercise: taking that monitor and integrating it into a system that was not written with Copilot in mind, so the property is actually enforced at run time inside a real application.

The feature list is a list of integrations, and each one names a host framework. Ogma generates NASA Core Flight System runtime monitoring applications that monitor data received from the message bus. It generates Robot Operating System runtime monitoring applications. It generates F Prime, F', runtime monitoring components. And it generates message handlers for cFS applications to make external data in structs available to a Copilot monitor.

Two of the entries are about the input rather than the host. Ogma can generate monitors from diagrams in diagrammatic formats, for example DOT/Graphviz and mermaid, and it can generate the glue code necessary to work with C structs in Copilot.

That last one is a quietly important capability. A Copilot monitor reasons about structured state, and a C application has its data in structs, and the two representations do not line up on their own. Generating the bridging code is what lets you state a property in terms of the application's own data rather than in terms of a parallel copy of it.

The two demonstration videos in the README are captioned as the integration of monitors into larger applications, with one showing monitoring within a simulation and the other showing monitoring within a robotics application, which is the two host worlds the tool was built for.

The project is written in Haskell, licensed under Apache-2.0, the default branch is develop, and the last push was on 2026-09-27 with releases v1.16.0 from 2026-09-22, v1.15.0 from 2026-07-22 and v1.14.0 from 2026-05-22.

The package layout is a list of front ends and back ends

The top level of the repository is where the design becomes visible, because the directories are named after the roles rather than after modules.

There is `ogma-cli/`, which is the command line program, `ogma-core/`, which holds the shared machinery, and `ogma-extra/`, which is where the extra pieces live. Then there is a family of `ogma-language-*` directories, and this is the interesting part of the layout. `ogma-language-c/` is the C language support, `ogma-language-copilot/` is the Copilot language support, `ogma-language-csv/` is CSV, `ogma-language-jsonspec/` is JSON spec, `ogma-language-lustre/` is Lustre, `ogma-language-smv/` is SMV, `ogma-language-xlsx/` is spreadsheet formats, and `ogma-language-xmlspec/` is XML spec.

So Ogma is a framework with pluggable front ends, one per input language or format, over a common core. The diagram support mentioned in the feature list is the DOT and mermaid path, and the CSV, JSON spec, SMV and Lustre paths are the other ways a property specification can arrive. The SpreadsheetML and XML spec directories are the two remaining front ends.

The `ogma-spec/` directory at the root is the specification layer, which is a distinct concern from the language front ends. A specification of what a monitor should check is separated from the languages in which a property can be written, and separating the two is what allows a new input format to be added without touching the generators.

The `cabal.project` file at the root ties the packages together for the Cabal build, and the whole set of directories is what `cabal install ogma-cli:ogma` resolves and builds. That is a Haskell multi-package layout, where each directory is a package rather than a module, and it is why the installation instructions ask for Copilot's own packages to be installed first as libraries.

The topic tags reinforce the intended domains: assurance, autonomy, cfs, embedded-systems, flight-software, fprime, robot-operating-system, robotics, ros, ros2, runtime-monitoring, runtime-verification, rv, space-ros and spacecraft. That is a project with one audience, namely people building software that has to be trusted and cannot afford a separate checker process.

Installing on Debian means a package, everywhere else means Cabal

The installation instructions split by platform, and the split is not cosmetic.

On Ubuntu 25.10 or Debian Forky or newer, Ogma can be installed directly from the package repositories with:

$ sudo apt-get install ogma

And to test that it is available, execute the following to print the list of commands supported:

$ ogma --help

On other Linux distributions or older Debian-based distributions, you must compile it from source. The prerequisites are a Haskell compiler, GHC, and the package manager Cabal, `cabal-install`, the libraries `bz2` and `expat`, and the theorem prover `z3`. The README recommends GHC 8.6 and a version of `cabal-install` between 2.4 and 3.2, and notes that Ogma has been tested with GHC versions up to 9.2 and cabal-install versions up to 3.6, although the installation steps may vary slightly depending on the version of `cabal-install` being used.

On Debian or Ubuntu the dependencies are:

$ apt-get install ghc cabal-install libz-dev libbz2-dev libexpat-dev z3

And once the compiler is installed, Ogma comes from Hackage:

$ cabal update
$ cabal install --lib copilot copilot-core copilot-c99 copilot-language \
    copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter
$ cabal install ogma-cli:ogma

The `ogma` executable then lands in `$HOME/.local/bin/`.

That long `--lib` line is the practical cost of this tool. The Copilot packages are installed as libraries rather than as executables because the generated monitors and the specifications link against the Copilot runtime, so the Copilot components have to be present on the system before Ogma is built. The dependency on z3 is the theorem prover Copilot uses, which means Ogma is not a self-contained code generator either; it needs a solver to reason about the property before it can generate the check.

For the development version, the README gives a git clone of the repository, a PATH export, and the same two cabal install steps.

Why the generated monitor has to be real-time C99

The choice of output language is the most consequential design decision in the project, and the README states it in one clause that is easy to skim past: Copilot is a high-level runtime verification framework that generates hard real-time C99 code.

Real time is the operative word. A runtime monitor sits inside the loop it is monitoring, so it has to meet the same deadlines as the code it watches. That rules out a monitor written in a managed language, and it rules out a monitor that calls out to a solver at run time. The monitor has to be a small, predictable function that inspects a few variables and signals a violation.

This is why z3 is a build-time dependency rather than a run-time one. The reasoning about the property happens when the monitor is generated, and what ends up in the application is compiled code with the reasoning already baked in. That is a very different artefact from a checker that re-derives the property each time it runs, and it is the reason the generated code can be hard real-time while the specification is written at a level where a human can reason about it.

It also explains the shape of the tool. If the output is code that must be integrated into somebody else's application, then the hard problems are not the property language at all, they are the integration: getting the right data into the monitor, dealing with the host's own types, and making the generated code fit the host's build and its memory constraints. That is what the feature list is mostly about, and it is why the list is organised by host framework, cFS, ROS and F Prime, rather than by feature of the monitor language.

The two demonstration videos make the same point visually. One is captioned as the integration of monitors into larger applications, for example simulators, and the other as the integration of monitors into robotics applications. Both are about the monitor living inside something, not about a checker looking at something from outside.

cFS, ROS and F Prime, and what each host needs from the monitor

The cFS section of the usage documentation explains what the NASA Core Flight System is and why it matters as a host.

The NASA Core Flight System, cFS, is a flight software architecture to implement complex systems by combining multiple reusable applications that communicate to one another via a software bus. cFS has been used, among others, on spacecraft, cubesats and drones.

That description of cFS is the key to understanding Ogma's role with it. In a cFS application, the data you want to monitor is not in one place, it is spread across applications communicating over a software bus. The monitor has to subscribe to the bus, receive the relevant messages, and maintain the state the property talks about.

That is what the feature list means by generating cFS applications that monitor data received from the message bus, and by generating message handlers for cFS applications to make external data in structs available to a Copilot monitor. The generated application is not a function you call, it is a participant in the message bus, and the handlers are what turn the bus traffic into the struct-shaped state the monitor reads.

The ROS target has the same shape of problem with a different vocabulary. A ROS application is a set of nodes publishing and subscribing to topics, and integrating a monitor means subscribing to the right topics and feeding the property with what they carry. The demonstration video for the ROS path shows monitoring within a robotics application, which is the case where the property is about a physical system rather than about a flight computer.

F Prime, written F', is the third target, and it appears both as a generated runtime monitoring component and in the topic tags. F Prime is a different kind of host from cFS, and the fact that Ogma supports all three is what makes it a framework rather than a one-off integration.

The three hosts together explain the tag list, which includes space-ros and spacecraft alongside ros, ros2 and robotics. The tool was built for flight software that shares a codebase with robotics, and the target list is the evidence of that.

Editorial conclusion

Adopt Ogma if your team already writes Copilot specifications and needs the monitors generated into a form that can run inside a flight software or robotics application rather than as a separate checker. Do not adopt it as a standalone runtime verification tool, because the generated code is the deliverable and the surrounding pipeline has to exist, and check first that your platform is one of the three it targets, since installation on anything other than recent Debian or Ubuntu means building from source with a specific GHC and Cabal combination.

Frequently asked questions

Official sources

1. Issues
2. License: Apache-2.0
3. nasa/ogma on GitHub
4. README
5. Releases