copilot: A stream DSL for writing embedded C programs.

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Copilot is a stream-based runtime verification framewor implemented as an embedded domain-specific language (EDSL) in Haskell. Programs can be interpreted for testing, or translated into C99 code to be incorporated in a project, or as a standalone application. The C99 backend output is constant in memory and time, making it suitable for systems with hard realtime requirements.

This package is the main entry-point for using Copilot.

A tutorial, examples, and other information are available at

[Skip to Readme]


Versions 0.21, 0.22, 0.23, 0.25, 0.26, 0.27, 0.28, 1.0, 1.0.1, 1.0.2, 2.0, 2.0.1, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.0.6, 2.0.7, 2.0.8, 2.0.9, 2.1.0, 2.1.1, 2.1.2, 2.2.0, 2.2.1, 3.0, 3.0.1, 3.1, 3.2, 3.2.1, 3.3, 3.3, 3.4, 3.5, 3.6
Change log CHANGELOG
Dependencies base (>=4.9 && <5), copilot, copilot-c99 (==3.3.*), copilot-core (==3.3.*), copilot-language (==3.3.*), copilot-libraries (==3.3.*), copilot-theorem (==3.3.*), directory (==1.3.*), filepath (==1.4.*), optparse-applicative (>=0.14 && <0.16) [details]
License BSD-3-Clause
Author Frank Dedden, Nis Nordby Wegmann, Lee Pike, Robin Morisset, Sebastian Niller, Alwyn Goodloe
Maintainer Frank Dedden <>
Category Language, Embedded
Home page
Bug tracker
Source repo head: git clone
Uploaded by IvanPerez at 2021-05-07T22:20:32Z



Manual Flags


Enable examples

Automatic Flags

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Maintainer's Corner

For package maintainers and hackage trustees

Readme for copilot-3.3

[back to package description]

Copilot: Stream DSL for hard real-time runtime verification

Build Status Version on Hackage

Copilot is a runtime verification framework written in Haskell. It allows the user to write programs in a simple but powerful way using a stream-based approach.

Programs can be interpreted for testing, or translated into C99 code to be incorporated in a project or as a standalone application. The C99 backend output is constant in memory and time, making it suitable for systems with hard realtime requirements.

Using Copilot

Assuming you have GHC and cabal already installed (see Haskell Platform or ghcup), there are several ways to use Copilot:

Note there is a TravisCI build (linked to at the top of this README) if you have trouble building/installing.


Here follows a simple example of a heating system. Other examples can be found in the examples directory of the main repository.

-- This is a simple example with basic usage. It implements a simple home
-- heating system: It heats when temp gets too low, and stops when it is high
-- enough. It read temperature as a byte (range -50C to 100C) and translates
-- this to Celcius.

module Heater where

import Language.Copilot
import Copilot.Compile.C99

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

-- External temperature as a byte, range of -50C to 100C
temp :: Stream Word8
temp = extern "temperature" Nothing

-- Calculate temperature in Celcius.
-- We need to cast the Word8 to a Float. Note that it 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"

The examples located in the examples/ directory can be run from the root of the project. Each example has a name. As a rule of thumb, the examples are named after the filename (without extension) in lowercase letters, and directory seperators replaced with a '-'. For example:

cabal run addmult -f examples
cabal run counter -f examples
cabal run what4-arithmetic -f examples


Feel free to open new issues and send pull requests.

In order to contribute to Copilot, please use the following steps which will make the process of evaluating and including your changes much easier:

This process is similar to Git Flow. The equivalent of Git Flow's master branch is our latest tag, and the equivalent of Git Flow's develop branch is our master.

Further information

For further information, including documentation and a tutorial, please visit the Copilot website:


We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National Institute of Aerospace, which partially supported this work.

Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported further development of Copilot.


Copilot is distributed under the BSD-3-Clause license, which can be found here.

The Copilot Team

The development of Copilot spans across several years. During these years the following people have helped develop Copilot (in no particular order):