Hi everyone!! We are really excited to announce Copilot 4.3 [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 runtime monitoring backend for NASA's Core Flight System, Robot Operating System (ROS2), FPrime (the software framework used in the Mars Helicopter). This release introduces several updates, bug fixes and improvements to Copilot: - Specifications now produce information about counterexamples when copilot-theorem is able to prove the property false. - We introduce a new Prop construct in copilot-core that captures the quantifier used in a property. - The What4 backend of Copilot theorem now produces an exception when trying to prove an existential property. The restriction of not being able to handle existentially quantified properties already existed, but due to information loss during the reification process, the quantifier was being lost and all properties to be proved via what4 were being treated as a universally quantified. - Several deprecated functions have been removed. - The installation instructions have been updated. - Compatibility with GHC 9.10 is now explicitly listed in the README. - Several typos have been fixed in comments and documentation. The new implementation is compatible with versions of GHC from 8.6 to 9.10. This release has been made possible thanks to key submissions from Ryan Scott (Galois) and Esther Conrad (NASA), the last of which is also a first-time contributor to the project. We are grateful to them for their timely contributions, especially during the holidays, and for making Copilot better every day. For details on this release, see [1]. https://github.com/Copilot-Language/copilot/releases/tag/v4.3. As always, we're releasing exactly 2 months since the last release. Our next release is scheduled for May 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, 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. Happy Haskelling! Ivan -- [1] https://github.com/Copilot-Language/copilot/releases/tag/v4.3 [2] https://hackage.haskell.org/package/copilot [3] https://github.com/nasa/ogma [4] https://github.com/Copilot-Language/copilot