// the find
nasa/ogma
Generator of runtime monitors for flight and robotics applications.
Ogma is a NASA-developed code generator that bridges formal runtime verification specs (written in Copilot, a Haskell DSL) with real flight and robotics frameworks — cFS, ROS/ROS2, and F'. You write the property in temporal logic; Ogma spits out the C99 glue code and framework scaffolding so the monitor actually runs on hardware. It's for aerospace/robotics engineers who need provably correct monitoring code without hand-writing message bus subscriptions.
- The separation between 'write the property once in Copilot' and 'generate platform-specific integration code' is the right abstraction — changing targets (cFS vs ROS vs FPrime) doesn't mean rewriting monitors, just re-running the generator.
- Copilot underneath generates hard real-time C99 with no heap allocation and no recursion — that's a real guarantee that matters in flight software, not marketing.
- The diagram-to-monitor path (mermaid/DOT → state machine → Copilot) means you can take a state chart from a systems engineer and generate verifiable C code from it directly, which closes a loop that usually requires manual translation.
- The variable DB + template system is genuinely extensible — projects can ship their own variable databases and custom templates without patching Ogma itself.
- The Haskell toolchain dependency is a real barrier: you need GHC, cabal, z3, and multiple Copilot libraries installed before you can do anything. On most Linux distros (anything older than Ubuntu 25.10) this is a multi-step manual process that will fail if versions don't align.
- ROS and F' support are explicitly labelled preliminary, and the current limitation is significant: Ogma generates the glue code but not the Copilot monitor implementation itself — you still have to place handwritten C files in specific directories, which partially defeats the automation.
- There's no feedback when a variable appears in a spec but has no matching entry in the variable DB — Ogma silently generates broken output rather than failing with an actionable error. That's a bug waiting to bite someone on a deadline.
- The `--parse-prop-via` LLM integration is a footgun: Ogma explicitly disclaims correctness of LLM-translated properties but will happily use the output without validation. In a safety-critical monitoring context, this needs much stronger guardrails or shouldn't exist.