Coq Platform
A dependable, cross-platform distribution of the Rocq proof assistant with a curated selection of libraries and tools.
What is Coq Platform?
Rocq Platform is a distribution of the Rocq proof assistant that packages Rocq with a curated set of libraries, plugins, and tools. It solves the problem of complex, platform-dependent installations by providing a unified, dependable setup across macOS, Windows, and Linux. The platform ensures users have a consistent, comprehensive environment for developing machine-checked proofs and formal verification projects.
Researchers, educators, and developers working in formal verification, theorem proving, or mathematical reasoning who need a reliable Rocq installation with essential libraries. It serves both beginners seeking an easy setup and experts requiring parallel version management.
Developers choose Rocq Platform for its cross-platform reliability, curated package selections, and support for parallel Rocq installations. It simplifies the often complex process of setting up Rocq and its ecosystem, offering a standardized, opam-based distribution that is both beginner-friendly and extensible for advanced use cases.
Overview
Multi platform setup for Coq, Coq libraries and tools
Use Cases
Best For
- Teaching formal verification and theorem proving courses with a pre-configured environment
Related Projects
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
