Copilot: writing runtime monitors in Haskell and shipping them as C99

Runtime verification as a compiled artifact

Copilot is a runtime verification framework for hard real-time systems. The two supported modes of use are the point of the whole design: programs can be interpreted for testing, or translated into C99 code to be incorporated into a project or a standalone application.

The property that matters is stated in the README: the C99 code generated is constant in memory and time, making it suitable for systems with hard real-time requirements.

That sentence is the difference between this and most runtime checking approaches. A monitor that allocates as it runs, or whose cost depends on how many events have accumulated, cannot be dropped into a deadline driven loop, because the check would then be a source of the very jitter you are trying to avoid. A monitor with constant time and constant memory can be scheduled like any other fixed cost task, which is what makes runtime verification usable in avionics, automotive and medical control loops rather than only in test harnesses.

The feature list spells out the rest of the workflow. Write simple, high-level specifications using a stream-based language. Produce hard real-time C99 runtime monitors. Catch errors in specifications early using an expressive static type system. Prove properties about specifications using theorem proving extensions. Interpret specifications for testing and debugging purposes. And obtain proofs of correctness of the generated code.

So the same artifact serves three audiences. The type checker finds specification errors before you run anything, the interpreter lets you debug the specification against simulated input, and the C code goes into the target system where it checks the real thing at runtime. The theorem proving and proof of correctness features sit on top for teams that need more than testing.

The audience is engineers working on systems where a missed condition has physical consequences. The topic list on the repository confirms the shape of it, with embedded-systems, requirements, requirements-engineering, runtime-assurance, runtime-monitoring and runtime-verification among the tags.

The repository is a family of packages, not one library

The repository layout is unusual for a Haskell project and tells you how the system is decomposed.

There is a top-level copilot directory, which is the umbrella package, and then a set of sibling packages: copilot-core, copilot-language, copilot-c99, copilot-interpreter, copilot-theorem, copilot-libraries, copilot-prettyprinter, copilot-verifier, copilot-bluespec and copilot-visualizer. A cabal.project file sits at the root to tie them together.

The names map onto the feature list. copilot-language holds the specification language itself, copilot-core the underlying machinery, copilot-c99 the backend that produces the C code, copilot-interpreter the execution engine for testing, copilot-theorem the theorem proving extensions, copilot-libraries the reusable specification fragments, and copilot-prettyprinter the code generation formatting. copilot-bluespec suggests a backend for a different hardware description target, and copilot-visualizer a way to see the generated monitors or their behaviour.

Splitting it this way matters for a practical reason: the installation instructions do not install a single package. They install eight of them by name, copilot, copilot-core, copilot-c99, copilot-language, copilot-theorem, copilot-libraries, copilot-interpreter and copilot-prettyprinter, with the --lib flag.

That list is effectively the set of things you need for the core workflow, and the reason for the split is that not everyone needs everything. The theorem proving extension is heavier than the runtime monitor generator, and the visualizer is a separate tool. A project that only wants to generate C99 monitors has no reason to pull in the proof machinery.

The website is at copilot-language.github.io, and the README points to API documentation and tutorials, a publications list, and a website, plus a section on contributions and acknowledgements that names the Copilot team and the institutional support behind the project.

Installing on Linux, Fedora and macOS

The install paths differ by platform, and the differences are worth knowing before you start.

On Debian Bookworm and Ubuntu 23.04 or newer, and on Fedora 40 or newer, Copilot is in the distribution package repositories. The Debian command is:

$ sudo apt-get install libghc-copilot-dev

and the Fedora equivalent is:

$ sudo dnf install ghc-copilot-devel

Both of those bring GHC with them, which is the point of the distribution packages. On other Linux distributions, or on older Debian based ones, you need a Haskell compiler and the Cabal package manager yourself. The supported compiler range is stated as GHC 8.6.5 up to modern versions, with 9.10 given as the current maximum on Linux, and the toolchain can be installed with ghcup. On Debian or Ubuntu the dependency set is:

$ sudo apt-get install ghc cabal-install alex happy pkg-config libz-dev

alex and happy are the standard Haskell lexer and parser generators, so they are needed because Copilot is a language implementation and parses its own source.

Once the compiler is in place, the Hackage install covers both the Linux generic path and macOS:

cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language \
    copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter

On macOS the toolchain comes from ghcup or from Homebrew with brew install ghc cabal-install, and the supported GHC range is 8.6.5 up to 9.6 as of the writing.

The verification step is the same everywhere, and it is a nice one to run because it does not need a file:

$ ghci <<< 'import Language.Copilot'

If the package is importable, the session ends with a line like ghci> ghci> Leaving GHCi. and prints no error messages.

For troubleshooting, the README points at the Travis CI file at the repository root and notes that issues often include Dockerfiles listing the steps needed to install Copilot from scratch, which is a practical route when the packaged installs do not fit your system.

A heating system example and what the generated files are

The README's example is a home heating system, and it is worth reading because it shows the shape of a specification rather than the shape of a program.

The specification reads an external temperature as a byte ranging from minus 50C to 100C, then converts it to Celsius:

-- This example implements a simple home heating system. The system heats
-- when the temperature gets too low, and stops when it is high enough. It
-- reads the temperature as a byte (range -50C to 100C) and translates it to
-- Celsius.

module Heater where

import Language.Copilot
import Copilot.Compile.C99

import Prelude hiding ((>), (<), div)

-- External temperature as a byte, ranging from -50C to 100C.
temp :: Stream Word8
temp = extern "temperature" Nothing

-- Temperature in Celsius.
--
-- We need to cast the Word8 to a Float. This is an unsafeCast, as there
-- is no direct relation between Word8 and Float.
ctemp :: Stream Float
ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0

spec = do
  -- Triggers that fire when the ctemp is too low or too high,
  -- pass the current ctemp as an argument.
  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
  trigger "heatoff" (ctemp > 21.0) [arg ctemp]

-- Compile the spec
main = reify spec >>= compile "heater"

Four things stand out. The external input is declared as a Stream Word8 bound to the name temperature, which is the interface the generated C will expose. The conversion uses unsafeCast, and the comment explains why, that there is no direct relation between Word8 and Float, so the cast bypasses the type system deliberately and the specification is what tells you the range is meaningful. The two triggers are conditions with names, and they carry the current value as an argument so the violation report includes the reading that caused it. And the entry point reifies the specification and compiles it to a target named heater.

Running it produces three files:

$ runhaskell Heater.hs

The output is heater.c, heater.h and heater_types.h, containing respectively the implementation of the monitors, the interface, and a declaration of any types declared in the specification, which is empty in this case.

That separation is the interface to the host system. The .h file is what you include, the .c file is what you compile and link, and the types header is the contract for any data the specification declares. A specification with no type declarations produces an empty types header, which keeps the integration surface minimal.

Examples live in the examples directory of the main repository, and there is a naming convention for running them: each example is named after its filename in lowercase with directory separators replaced by a dash, run from the root of the project, for example cabal run addmult -f ex.

Why the Haskell dependency is the real cost

Copilot's technical case is strong, but the honest evaluation has to start with the toolchain requirement, because that is what determines whether a team can use it.

To adopt Copilot you need GHC and Cabal, and depending on the platform, alex and happy, pkg-config and libz-dev, or the distribution packages that bundle GHC. Every one of those is a real dependency on a Haskell toolchain in an organization that may not otherwise have one. The build produces a C artifact, which is the point, but the specification is written and maintained in Haskell.

That has a second implication that the README does not spell out. The specification is a Haskell value, so it is type checked by GHC before it is ever interpreted or compiled. The feature list calls this out as catching errors in specifications early using an expressive static type system, and the Prelude hiding in the example is there because the specification language has its own comparison and division operators that would otherwise clash with the standard ones. That clash is a small illustration of what living inside Haskell means in practice: the DSL is a Haskell library, so it inherits Haskell's name resolution and operator set.

The other structural cost is the size of the generated monitor. Constant memory and time is a guarantee about the cost per step, not about the total size of the code. A monitor with a hundred triggers and a complicated state machine produces a larger C file, and in a memory constrained embedded target that is a real budget item you need to check rather than assume.

The alternatives each trade differently. Writing the monitor by hand in C gives full control and no toolchain, and it is the right answer when the check is simple enough to be obvious, such as a single range comparison on a sensor value. A property based testing approach checks properties offline against a simulator rather than online against the running system, which is far cheaper to adopt but catches violations only when the test exercises the condition. And a formal verification toolchain that proves the design satisfies its specification outright gives a stronger guarantee than runtime monitoring, at a much higher cost in modelling effort and in the expertise required.

Copilot occupies a specific middle position: runtime assurance, where the monitor runs alongside the system and catches a violation at the moment it happens. It is a different guarantee from offline testing, because the check applies to the real system in the real environment, including faults the test never produced.

Licence, versions and what to check first

Two practical notes for anyone about to commit to this.

The first is the licence. The repository's licence is recorded as unknown, and the README does not include a licence section. For a framework whose output is compiled into your own system rather than distributed as a service, that is a different question from a web service, but it is still a question. The C code you generate belongs to you, since it is derived from your specification, but the compiler itself is what carries the licence, and you should read the terms before embedding it in a product you ship.

The second is the release line. The listed releases are v4.8.1 from 2026-09-08, v4.8 from 2026-07-08 and v4.7.1 from 2026-05-08, so the 4.x line is moving regularly. The repository is not archived and the last push was on 2026-10-18, which is days ago.

What to check first, concretely. Compile the generated C99 with your actual target compiler and its warning flags, because the generated code is machine produced and your toolchain is the one that has to accept it. Then confirm the external input contract matches your system, since the name you bind with extern is the name the host code has to supply, and a mismatch is a link time or a silent wrong value rather than a clear error. Then size the monitor against your memory budget, since constant per step cost does not mean small.

And test the interpreter mode first. The whole point of being able to interpret a specification is that you can exercise it against simulated input before it ever runs in the target, and it is far cheaper to find a specification error there than in the deployed system.

For the team behind it, the README acknowledges both the Copilot team and the institutional support, and points to the publications list, which is the place to look if you want to understand the theoretical basis for the generated code before you depend on it.

Editorial conclusion

Adopt Copilot if you build safety critical or hard real-time systems and your team can carry a Haskell toolchain, because the guarantee that the generated monitor runs in constant time and memory is what makes it usable in a deadline-driven loop. Do not adopt it for ordinary application code, where a runtime assertion library or a test suite would do the same job with less machinery. Verify first that your target compiler accepts the generated C99, that your platform provides the external inputs the specification expects, and that the size of the generated monitor fits the memory budget you have for it.

Frequently asked questions

Official sources

1. Copilot-Language/copilot on GitHub
2. Issues
3. Project website
4. README
5. Releases