Copilot is a realtime programming language and Runtime Verification framework. It allows users to write concise programs in a simple but powerful way using a stream-based approach.

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

Learn more about the project... 

-- Raw temperature from sensor, range -50.0C to 100.0C.
temp :: Stream Word8
temp = extern "temperature" Nothing

-- Transform the temperature to Celsius.
ctemp :: Stream Float
ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0

-- Bind two triggers with a 3.0C hysteresis.
spec = do
  trigger "heaton"  (ctemp < 18.0) [arg ctemp]
  trigger "heatoff" (ctemp > 21.0) [arg ctemp]

News

Release 4.7.1 – 2026-05-07

We are pleased to announce the release of Copilot 4.7.1, a stream-based DSL for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. Copilot is typically used as a high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), clocks and voting algorithms.

Among others, Copilot is being used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones.

This release introduces several improvements to Copilot:

We expect those new modules to grow in the future.

The new implementation is compatible with versions of GHC from 8.6 to 9.10, as well as with Stackage Nightly.

This release has been made possible thanks to key submissions from Ryan Scott (Galois), and Chris Hathhorn (Galois). We are grateful to them for their timely contributions, and for making Copilot better every day.

Details are available here, and here.

As always, we’re releasing exactly 2 months since the last release. Our next release is scheduled for Jul 7th, 2026.

We want to remind the community that Copilot is now accepting code contributions from external participants again. Please see the discussions and the issues to learn how to participate.

Current emphasis is on improving the codebase in terms of performance, stability and test coverage, removing unnecessary dependencies, hiding internal definitions, formatting the code to meet our new coding standards, and simplifying the Copilot interface. Users are encouraged to participate by opening issues, asking questions, extending the implementation, and sending bug fixes via our github repo.

License

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

Acknowledgements

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.

We would like to thank Kaveh Darafsheh (NASA Langley Research Center) for his help with testing Copilot. In addition numerous people have helped with smaller things, reporting bugs etc. Thanks to all of them!