[Copilot] is a realtime programming language and Runtime Verification
framework. It allows users to write concise programs in a simple
but powerful way using a stream-based approach. Programs can be
interpreted for testing, or translated C99 code to be incorporated
in a project, or as a standalone application. Есть для ардуины и
для RTOS Zephyr. Внутри Haskell, но генерит plain C99. Система
верификации использует как темпоральную логику (в двух вариантах),
так и
решатели теорем.
https://copilot-language.github.io/about.html
https://hackage.haskell.org/package/arduino-copilot
https://hackage.haskell.org/package/zephyr-copilot
https://github.com/Copilot-Language/Copilot/
https://hackage.haskell.org/package/copilot-language