Rocq Long Term Roadmap

Vision:

The Rocq Development Team, building on 40 years of experience with Coq, is pleased to announce the Rocq Prover, the next-generation proof assistant. The Rocq Prover is designed to empower a diverse range of users, from mathematicians seeking formal rigor to software engineers building high-assurance systems.

While Rocq leverages the rich heritage of Coq, it embraces a more agile development philosophy. This allows us to deliver impactful changes more frequently, accelerating innovation and user experience improvements.

This roadmap outlines our vision for Rocq’s future, focusing on four key pillars:

Join us in shaping the future of formal verification!

Target Audiences:

A,B,C,D,E are used hereafter to refer to the target audiences of each feature, references are given at the end of this roadmap.

1. Open and Accessible

2. Trustworthy Proofs

3. Implementation Efficiency and Maintainability

4. Enhanced Usability

This roadmap represents our ongoing commitment to making the Rocq Prover a powerful, user-friendly, and reliable proof assistant for a broad range of users. We welcome feedback and contributions from the community to help us achieve this vision.


References: