<div dir="ltr">Hi everyone!!<br><br>We are really excited to announce Copilot 4.3 [1,2]. Copilot is a<br>stream-based EDSL in Haskell for writing and monitoring embedded C<br>programs, with an emphasis on correctness and hard realtime<br>requirements. Copilot is typically used as a high-level runtime<br>verification framework, and supports temporal logic (LTL, PTLTL and<br>MTL), clocks and voting algorithms. Compilation to Bluespec, to<br>target FPGAs, is also supported.<br><br>Copilot is NASA Class D open-source software, and is being used at NASA<br>in drone test flights. Through the NASA tool Ogma [3] (also written in<br>Haskell), Copilot also serves as a runtime monitoring backend for<br>NASA's Core Flight System, Robot Operating System (ROS2), FPrime (the<br>software framework used in the Mars Helicopter).<br><br>This release introduces several updates, bug fixes and improvements to<br>Copilot:<br><br>- Specifications now produce information about counterexamples when<br>  copilot-theorem is able to prove the property false.<br><br>- We introduce a new Prop construct in copilot-core that captures the<br>  quantifier used in a property.<br><br>- The What4 backend of Copilot theorem now produces an exception when<br>  trying to prove an existential property. The restriction of not being<br>able to handle existentially quantified properties already existed, but<br>due to information loss during the reification process, the quantifier<br>was being lost and all properties to be proved via what4 were being<br>treated as a universally quantified.<br><br>- Several deprecated functions have been removed.<br><br>- The installation instructions have been updated.<br><br>- Compatibility with GHC 9.10 is now explicitly listed in the README.<br><br>- Several typos have been fixed in comments and documentation.<br><br>The new implementation is compatible with versions of GHC from 8.6 to<br>9.10.<br><br>This release has been made possible thanks to key submissions from Ryan<br>Scott (Galois) and Esther Conrad (NASA), the last of which is also a<br>first-time contributor to the project. We are grateful to them for<br>their timely contributions, especially during the holidays, and for<br>making Copilot better every day.<br><br>For details on this release, see [1].<br><a href="https://github.com/Copilot-Language/copilot/releases/tag/v4.3">https://github.com/Copilot-Language/copilot/releases/tag/v4.3</a>.<br><br>As always, we're releasing exactly 2 months since the last release. Our<br>next release is scheduled for May 7th, 2025.<br><br>We want to remind the community that Copilot is now accepting code<br>contributions from external participants again. Please see the<br>discussions and the issues in our github repo [4] to learn how to<br>participate.<br><br>Current emphasis is on using Copilot for full data processing<br>applications (e.g, system control, arduinos, rovers, drones), improving<br>usability, performance, and stability, increasing test coverage,<br>removing unnecessary dependencies, hiding internal definitions,<br>formatting the code to meet our new coding standards, and simplifying<br>the Copilot interface. Users are encouraged to participate by opening<br>issues, asking questions, extending the implementation, and sending bug<br>fixes.<br><br>Happy Haskelling!<br><br>Ivan<br><br>--<br><br>[1] <a href="https://github.com/Copilot-Language/copilot/releases/tag/v4.3">https://github.com/Copilot-Language/copilot/releases/tag/v4.3</a><br><br>[2] <a href="https://hackage.haskell.org/package/copilot">https://hackage.haskell.org/package/copilot</a><br><br>[3] <a href="https://github.com/nasa/ogma">https://github.com/nasa/ogma</a><br><br>[4] <a href="https://github.com/Copilot-Language/copilot">https://github.com/Copilot-Language/copilot</a></div>