It is well established that errata in the real-time scheduling literature are not uncommon (e.g., refer to the discussion and examples provided by Cergueira et al., 2016; Bedarkar et al., 2022; and Maida et al., 2022). For a field that claims applicability in the design and validation of safety-critical systems, that is a major problem.
When should engineers trust published analysis results? What tooling can actually be relied on? Mechanization with a proof assistant (such as Rocq) provides a path towards restoring confidence in the correctness of fundamental scheduling theory.
Worse, the issue of analysis correctness is unlikely to get any better by itself:
For the scientific real-time systems community to have impact in the long run, we collectively need to build up infrastructure and methodologies for detailed, yet trustworthy analyses. Prosa is one attempt at creating such a foundation.
While we naturally have to start with simpler models and analyses in this endeavor, the ambition is to scale to much more refined models applicable to real systems. For an example of this, see the work by Bedarkar et al. (2025) on RefinedProsa.
There are many ways in which one could possibly employ a proof assistant to formalize real-time scheduling. Not all such approaches are equally suited for all purposes, nor equally well understood by all audiences. Prosa is squarely aimed at an audience without much prior experience with formal proofs, guided by the following goals and principles.
To ensure that Prosa is useful and yet feasible in the long term, is design is informed by three basic goals.
The envisioned scope of Prosa is real-time scheduling theory, as one might find it in a modern textbook on real-time systems.
Prosa is an open-source project to enable peer review and community involvement. As a long-term goal, we envision a shared repository of formal definitions and proofs of major results in real-time scheduling that goes beyond the effort of any single group.
By providing Rocq-verified schedulability analysis, we hope to further the adoption in practice of modern real-time resource management approaches, especially in the context of safety-critical systems subject to certification requirements.
Given that the literature on real-time scheduling is vast, we focus our finite resources on those aspects of scheduling theory that are most relevant from a safety perspective. In particular, in schedulability proofs, we prioritize sufficient over necessary conditions, and typically do not formalize results on other secondary issues such as whether analysis algorithms are guaranteed to terminate or their time complexity.
The scenario that must be prevented at all costs is the use of unsound analysis for the validation of safety-critical systems: unsound analysis can produce incorrect results that might go unnoticed at validation time, but lead to system failure down the line.
In contrast, the failure modes of other possible issues — such as a fixed-point search that fails to converge, accidental pessimism, or an erroneously derived time or memory complexity bound — are either readily apparent to the engineer (e.g., the analysis times out or unexpectedly claims a system to be unschedulable), or are of interest only to the academic community and cannot result in failures in deployed systems.
Nevertheless, Prosa is expressive enough to define and prove some of these additional properties, and is happy to accept such contributions (e.g., Prosa contains a proof of the optimality of EDF, even though that is not safety-relevant).
Prosa specifically targets researchers seeking to develop and publish provably-correct schedulability analyses. Engineers and other practitioners working on specific real-time systems in their day-to-day work are not the primary audience, and will instead indirectly benefit from the artifacts of this research.
In particular, tool providers can implement analyses that are guaranteed to be correct, and can also test their implementations against provably correct reference models in Prosa. As a result, end users will eventually benefit from better tools and safer systems. For concrete examples of this, refer to the work on CertiCAN and POET.
To become and remain as accessible as possible, Prosa sticks to the following principles.
The correctness of a mechanized proof only goes as far as the fidelity of the underlying specification, which must still be manually vetted and accepted as valid by the community at large. Hence, formal definitions and theorem statements should be as easily understood as their pen-and-paper counterparts.
Our primary goal is to make the specification accessible to researchers familiar with real-time scheduling who do not necessarily have a background in formal methods. As part of our coding style, we favor the following guidelines.
Many lemmas, short proofs: To make proof strategies easy to follow, we split the proof of theorems into many short lemmas (so that each proof script spans at most a few dozen lines of code). This makes it possible to understand the proof outline at a high level without diving into low-level proof scripts.
Long, verbose names: Our definitions and lemmas have verbose names to make statements self-contained and clear, so that the flow of the proof can be easily followed even without understanding each formal definition in detail.
Heavy use of documentation: We use Rocq documentation facilities (e.g., coqdoc) to make the experience of reading a specification closer to that of reading a paper. In particular, we intersperse paper-like explanations and matching formal statements to provide guidance to the reader.
See also the Prosa writing and coding guidelines.
Excessive generality and abstraction can harm readability, as it creates clutter, indirection, and numerous dependencies across many files and definitions. In contrast to traditional software engineering guidelines, it can be beneficial to allow for some degree of redundancy in the interest of immediacy and accessibility.
Prosa intentionally favors novice readers of the specification (who can focus on the subject matter, i.e., scheduling and questions of timeliness) over experienced authors of specifications and proofs (who are forced to produce more code). This is a deliberate choice in line with the observation that formal proofs are of limited value if they are ignored by the community at large — to be successful, a formal specification must be read much more often than it is written.
Instead of radically changing the way that proofs are carried out (e.g., by switching to temporal logics that are expressive, but not universally understood), we believe that a universal formal specification of real-time scheduling should reuse the common concepts and proof style established by the community in the past four decades. Doing so not only allows existing results to be more easily formalized, but also makes our formalization of scheduling concepts more accessible to readers with prior knowledge of the literature on real-time scheduling.
In our specification, we seek to mostly avoid complex Rocq features that go beyond common mathematical concepts, other than in a few exceptional cases for simplicity or compatibility with libraries. Rather, we favor basic concepts that are readily familiar to any computer scientist such as first-order logic, lists, functions, and Peano arithmetic.
(That said, the full power of Rocq remains available for any concepts and proofs that do not easily fit into these confines.)