[Haskell-cafe] [ANN] Copilot 3.19.1

Frank Dedden frank at systemf.dev
Tue May 14 18:53:10 UTC 2024


Hi everyone!

We are very excited to announce Copilot 3.19.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.

Copilot marked as 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 runtime monitoring backend for NASA's Core
Flight System, Robot Operating System (ROS2), and FPrime (the software
framework used in the Mars Helicopter).

This release does not contain any API breaking changes, but consists of some
improvements to the copilot-theorem package. Thanks to Ryan Scott (Galois Inc.)
a problem related to the interface with the Kind 2 model checker is fixed.
Additionally, improvements have been made to the documentation.

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

Current emphasis is on improving the codebase in terms of stability and
test coverage, removing unnecessary dependencies, hiding internal
definitions, and formatting the code to meet our new coding standards.
Additionally, as an ongoing process, work is being done on making Copilot more
accessible to people less familiar with Haskell.
Users are encouraged to participate by opening issues and asking questions via
our github repo [4].

Happy Haskelling!

Frank Dedden


[1] https://github.com/Copilot-Language/copilot/releases/tag/v3.19.1

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

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

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



More information about the Haskell-Cafe mailing list