Get Prosa

There are three main ways to use Prosa: either read the specification online (recommended for novices and researchers with a casual interest), download and check a specific release, or clone the Prosa repository (recommended for development).

Read the Prosa Specification

The recommended way to read Prosa is by looking at the HTML specification with low-level proofs hidden (available on demand by clicking “Proof” under each lemma/theorem):

If you are unsure where to start, then read the specifications in the module prosa.behavior first, followed by those in prosa.model. The release overview provides further information on the organization of the Prosa library.

Note: if the specification appears to be missing all comments, try reloading the page with your ad-blocker disabled; there are some false-positive issues with coqdoc and certain blockers.

Checking the Proofs

To independently verify the correctness of the proofs, the full development can be downloaded, compiled, and validated with the Coq proof checker. This process is intentionally very simple and does not require any prior Coq knowledge.

  1. Make sure you have a working Coq installation with all prerequisites installed — if you do not, please check the setup instructions.
  2. Check out (or extract from the downloaded ZIP file) the version of Prosa you would like to check. To check the latest development version of Prosa, simply run git clone
  3. In the Prosa directory created in the previous step, create a Makefile by running ./ For further information on this poin, see also the compilation instructions).
  4. Run make validate.

The last step should report that there are no unproven or admitted theorems, nor any nonstandard axioms. For a short tutorial on how to interpret the output, please consult the ECRTS’16 artifact evaluation instructions.

The Prosa Repository

To start a new proof development or to contribute patches, it’s best to work with the Prosa git repository, which is publicly available on the MPI-SWS GitLab server.

Up-to-date documentation for all branches is generated automatically.

To clone the repository, use the following command.

git clone

For a tutorial on how to compile Prosa, please follow the setup instructions.


We infrequently provide stable releases, which may be found below. Note that these releases are primarily intended as stable snapshots for ease of reference (e.g., to refer to a specific proof in a paper). For new developments, general improvements, or simply getting to know Prosa, please base your work on the current version (as found in the git repository).

The current releases of Prosa are usually based on the latest versions of Coq and the Mathematical Components library (mathcomp). For a step-by-step guide on how to install Prosa and its dependencies, please check out the setup instructions.

Prosa 0.5

Released on November 7, 2022. Tested with Coq 8.16.0 and mathcomp 1.15.0.

Prosa 0.4

Released on December 21, 2019. Tested with Coq 8.10.0 and mathcomp 1.9.0.

Prosa v0.4 is the first release of the completely refactored “new Prosa”. The prior version is still available in the “classic” namespace, but it is deprecated and will not be developed any further. Eventually, the classic version will be removed.

Prosa 0.3

Released on July 17, 2018. Tested with Coq 8.7.0 and mathcomp 1.6.4.

Prosa v0.3 introduces the new classification of strong and weak sustainable policies. It also includes a proof that uniprocessor JLFP scheduling of self-suspending tasks is weakly sustainable with respect to execution times and variable suspension times. See the overview page for more information.

Prosa 0.2

Released on June 6, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.

Prosa v0.2 incorporates the reduction-based response-time analysis (RTA) for real-time scheduling with arbitrary processor affinities (APA). See the overview page for more information.

Prosa 0.1

Released on May 5, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.

Prosa v0.1 formalizes Bertogna and Cirinei’s response-time analysis (RTA) for global FP and EDF scheduling, along with extensions for release jitter and parallel jobs. For additional information, please follow the ECRTS’16 artifact evaluation instructions.