Hi everyone!!

We are really excited to announce Copilot 4.5.1 [1,2]. Copilot is a
stream-based EDSL in Haskell 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. Compilation to Bluespec, to target
FPGAs, is also supported.

Copilot is NASA Class D open-source software, and is being used at NASA
in drone test flights. Through the NASA tool Ogma [3] (also written in
Haskell), Copilot also serves as a programming language and runtime
framework for NASA's Core Flight System, Robot Operating System (ROS2),
FPrime (the software framework used in the Mars Helicopter). Ogma now
supports producing flight and robotics applications directly in
Copilot, not just for monitoring, but for implementing the logic of the
applications themselves.

Since the last announcement, the major updates and improvements are:

- Copilot maintream now includes the verification, FPGA and
  visualization backends.

- Copilot now includes a tutorial showing how to generate code for FPGA
  and run it (thanks to Sukhman Kahlon!).

- Compatibility with newer versions of dependencies has been extended.

- Cleaning efforts in `copilot-theorem`, and `copilot-core`.

A picture of the Copilot visualizer can be seen at [5].

The new implementation is compatible with versions of GHC from 8.6 to
9.12.

This release has been made possible thanks to key submissions from
Sukhman Kahlon (NASA). We also thank Corey Carter (NASA), Ryan Scott
(Galois) and Kaveh Zare (NASA) for their input. We are grateful to them
for their contributions, and for making Copilot better every day.

For details on this release, see [1].

As always, we're releasing exactly 2 months since the last release. Our
next release is scheduled for Nov 7th, 2025.

We want to remind the community that Copilot is now accepting code
contributions from external participants again. Please see the
discussions and the issues in our github repo [4] to learn how to
participate.

Current emphasis is on using Copilot for full data processing
applications (e.g, system control, arduinos, rovers, drones), improving
usability, performance, and stability, increasing test coverage,
removing unnecessary dependencies, hiding internal definitions, and
formatting the code to meet our coding standards. Users are encouraged
to participate by opening issues, asking questions, extending the
implementation, and sending bug fixes.

Happy Haskelling!

Ivan

--

[1] https://github.com/Copilot-Language/copilot/releases/tag/v4.5.1

[2] https://hackage.haskell.org/package/copilot

[3] https://github.com/nasa/ogma

[4] https://github.com/Copilot-Language/copilot

[5] https://www.reddit.com/r/haskell/comments/1nci0u6/ann_copilot_451/