
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