Copilot is a hard realtime C code generator and runtime verification framework written in Haskell. It has been developed by researchers at the National Institute of Aerospace, Galois Inc., and NASA Langley Research Center.
Although I was not part of the initial development of Coilot, I have redesigned and reimplemented the code generator / compiler, and extended the language. Currenly I share the maintainership with Alwyn Goodloe of NASA Langley.
For downloads, source code and further information, please see Copilots webage: https://copilot-language.github.io.