The Coq Proof Assistant

For many years, the development of Coq has been supported and funded almost exclusively by French academic institutions, most notably Inria. But today, there are intensive Coq users, and thus major stakeholders, in universities and companies all over the world.

The objective of the Consortium is to empower this community of users, whose research and development critically rely on the Coq system. For these users, making sure that the system's maintenance is well funded is essential. They can do so by providing resources either as donations, Consortium membership or support service subscriptions. Furthermore, Consortium members and support service subscribers get a voice in the evolution of Coq, by determining where some engineering resources are allocated.

To summarize, 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 major stakeholders are addressed efficiently by providing a fantastic working environment to competent Coq developers.

The Coq Consortium is hosted by Inria (the French national institute for research in digital science and technology), the premier actor behind the development of Coq.

If you wish to financially support the development of Coq and its community, you can make a donation to Inria. Please contact us.

The Coq Consortium comprises the following levels of Membership, depending on a yearly financial contribution:

• Gold membership: 20k€
• Platinum membership: 50k€

This contribution supports the development of Coq, on priorities defined by the Consortium assembly. Gold members get one vote for each ballot at the assembly, Platinum members get three votes.

If you wish to join the Coq Consortium as a member, please contact us.

Partners can subscribe a package of support services:

• Premium support for bugs. Reports will be processed in priority by the Consortium engineers.
• Integration of client code in regression tests.
• Privileged access to Coq developers via a dedicated mailing list.
• Advertisement of the partner’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 partners are eligible to a 50% discount.