The Coq Consortium

A pool of resources and a platform for exchanges

The objective of the Consortium is to make the community of users feel empowered with respect to the future of the Coq system, giving them opportunities to see how the system will evolve, where it is going, and to take an active part in this process. On the one hand, we wish to establish transparent ways of contributing financially and technically to the development of the system; on the other hand we wish to make sure that the most pressing needs of the user community are addressed efficiently by providing a fantastic working environment to competent developers.

Support services

The Consortium provides a package of support services:

  • Premium support for bugs. Reports by Consortium members will be processed in priority by the Consortium engineers. Private bug reports can be processed by Consortium engineers under an NDA to explore a code base and minimize a bug example.
  • A session of on-site training each year. (Optional, travel and lodging expenses should be paid by the member).
  • Integration of some code from members in regression tests.
  • Privileged access to Coq developers via a dedicated mailing list.
  • Advertisement of the member’s involvement in the Coq community.

Partners declare a number of intensive users of Coq they represent, and the Consortium recommends a corresponding level of service (a number of engineer hours, which can be used for support or training). The cost corresponds to that specific level of service. Academic members receive a 50% discount.

UsersEngineer hours1 year2 years3 years
5-7 4h/user/year € 2000/user € 3600/user € 4800/user
8-12 32h/year € 16000 € 28800 € 38400
13-14 36h/year € 18000 € 32400 € 43200
15+ 40h/year € 20000 € 36000 € 48000

Beside these services, the Consortium can establish contracts with members to audit code and emit a quality label if the audit is successful. The Consortium can also certify Coq related services like training and support provided by members.

Hosted by a non-profit foundation

The Coq Consortium is hosted by a non-profit foundation associated to Inria providing engineering resources for the development of software created in research teams. This set-up makes it possible for the Coq Consortium to receive donations or establish specific support contracts.

How to join?

The Coq Consortium is currently being created by the Inria Foundation. If you are interested, please contact Yves Bertot or Maxime Dénès.

Note: the information contained in this document is not contractual and may be subject to change. All prices listed are in Euros and are subject to changes and printing errors.