F42 Change Proposal: Copilot Runtime Verification Framework (self-contained)

Project Discussion Change Proposals
,
1

The Copilot Runtime Verification Framework

This is a proposed Change for Fedora Linux.
This document represents a proposed Change. As part of the Changes process, proposals are publicly announced in order to receive community feedback. This proposal has been previewed by the Fedora Engineering Steering Committee and members of Fedora QA as it is a late change, and has been provisionally approved as acceptable for F42 release, pending community feedback. If any feedback is received that alters the change proposal in a significant way, it will be resubmitted to FESCo for a further review and vote.

Wiki
Announced

:link: Summary

Copilot Language and Runtime Verification System is a stream-based runtime-verification framework for generating hard real-time C code.

:link: Owner

:link: Detailed Description

Copilot is a realtime programming language and Runtime Verification framework, developed for NASA. 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. The C99 backend ensures us that the output is constant in memory and time, making it suitable for systems with hard realtime requirements.

:link: Feedback

:link: Benefit to Fedora

This is a new feature in Fedora which will of interest to those developing specific critical embedded systems requiring a high level of software assurance.

:link: Scope

  • Proposal owners:

    • build the copilot stack for Rawhide/F42: version 3.19 is packaged [done]

  • Other developers:

  • Release engineering: #Releng issue number

  • Policies and guidelines: N/A (not needed for this Change)

  • Trademark approval: N/A (not needed for this Change)

  • Alignment with the Fedora Strategy:

:link: Upgrade/compatibility impact

:link: Early Testing (Optional)

Do you require ‘QA Blueprint’ support? Y/N

:link: How To Test

  • sudo dnf install ghc-copilot-devel
  • follow the documentation below for tutorial examples

:link: User Experience

Users will be able to easily install the Copilot verification framework and test it.

:link: Dependencies

:link: Contingency Plan

  • Contingency mechanism: (What to do? Who will do it?) N/A (not a System Wide Change)
  • Contingency deadline: N/A (not a System Wide Change)
  • Blocks release? N/A (not a System Wide Change), Yes/No

:link: Documentation

Last edited by @amoloney 2025-03-10T12:22:22Z

Last edited by @amoloney 2025-03-10T12:22:22Z

2

How do you feel about the proposal as written?

  • Strongly in favor
  • In favor, with reservations
  • Neutral
  • Opposed, but could be convinced
  • Strongly opposed
0 voters

If you are in favor but have reservations, or are opposed but something could change your mind, please explain in a reply.

We want everyone to be heard, but many posts repeating the same thing actually makes that harder. If you have something new to say, please say it. If, instead, you find someone has already covered what you’d like to express, please simply give that post a :heart: instead of reiterating. You can even do this by email, by replying with the heart emoji or just “+1”. This will make long topics easier to follow.

Please note that this is an advisory “straw poll” meant to gauge sentiment. It isn’t a vote or a scientific survey. See About the Change Proposals category for more about the Change Process and moderation policy.

3

You mean F43?

2 Likes