What is Copilot? Copilot is a runtime verification framework for hard real-time systems. You can write business logic in a high-level streaming DSL, and Copilot will translate it into C99 code, which can be directly integrated into your project. The generated monitors have constant memory and execution time, making it a boon for embedded systems with stringent hard real-time requirements.
What pain points does it address?
| Pain Point | Copilot’s Solution |
| Inconsistency between requirements and implementation | Write requirements directly as specifications in a streaming language, automatically generating monitoring code at compile time for real-time comparison. |
| High debugging costs | Specifications can be run in an interpreter, allowing you to see outputs in real-time, saving you from the torment of repeatedly refreshing code. |
| Monitoring overhead in hard real-time systems | C99 code has constant memory/time, ensuring it won’t freeze the system. |
| Difficult error localization | The static type system captures most errors at compile time, avoiding runtime crashes. |
| Lack of formal guarantees | The built-in theorem proving extension can provide correctness proofs for specifications, enhancing reliability. |
Let’s get it installed!
- • Linux (Debian/Ubuntu)
sudo apt-get install libghc-copilot-dev ghci <<< 'import Language.Copilot' - • Fedora
sudo dnf install ghc-copilot-devel ghci <<< 'import Language.Copilot' - • Other Linux (or if you want to experiment) First install GHC + Cabal (
<span>ghcup</span>or apt), then run:cabal v2-install --lib copilot copilot-core copilot-c99 \ copilot-language copilot-theorem copilot-libraries \ copilot-interpreter copilot-prettyprinter - • macOS (Homebrew)
brew install ghc cabal-install cabal v2-install --lib copilot …
After installation, open ghci and if <span>import Language.Copilot</span> returns successfully, you are good to go. Next, you can write <span>.hs</span> files and use <span>reify spec >>= compile "mymonitor"</span> to compile the specification into C code, which can be directly integrated into your MCU project.
Pros and Cons Overview
| Pros | Cons |
| Normalized, readable DSL, separating business logic and monitoring | Higher entry barrier, requires basic knowledge of Haskell |
| Constant time/space C99 monitoring code | Generated code may still require manual optimization for extremely resource-constrained scenarios |
| Static type system catches errors early | Integration with existing toolchains (like Simulink) is not yet mature |
| Supports interpreter debugging & theorem proving | Community and Chinese resources are relatively scarce, requiring self-exploration |
| Multi-platform support (Linux/macOS) | Windows support is not user-friendly, requiring WSL or a virtual machine |
Conclusion If you are struggling with safety monitoring for embedded hard real-time systems, Copilot is definitely worth a try. It integrates requirements directly into the code, making monitoring not an afterthought but part of the business code that is compiled and deployed together. Although the learning curve is a bit steep, once you get the hang of it, you’ll find the satisfaction of having code that can directly validate requirements is truly rewarding. Don’t forget, the power of the open-source community awaits your contributions—whether it’s bugs, documentation, or new features, you can directly submit your changes via PR.
Project Address: https://github.com/Copilot-Language/copilot