package rocq-prosa

Prosa is a repository of definitions and proofs for real-time schedulability analysis. Prosa’s distinguishing characteristic is that Prosa prioritizes readability over all other concerns to ensure that specifications remain accessible to readers without a background in formal proofs. (A background in real-time scheduling is assumed.)