Rocq Prover (was known as Coq) is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
Users generate proofs by entering a series of tactics that constitute steps in the proof. There are many built-in tactics, some of which are elementary, while others implement complex decision procedures (such as lia, a decision procedure for linear integer arithmetic). Ltac and its planned replacement, Ltac2, provide languages to define new tactics by combining existing tactics with looping and conditional constructs. These permit automation of large parts of proofs and sometimes entire proofs. Furthermore, users can add novel tactics or functionality by creating Rocq plugins using OCaml.
The Rocq kernel, a small part of Rocq, does the final verification that the tactic-generated proof is valid. Usually the tactic-generated proof is indeed correct, but delegating proof verification to the kernel means that even if a tactic is buggy, it won’t be able to introduce an incorrect proof into the system.
Finally, Rocq also supports extraction of verified programs to programming languages such as OCaml and Haskell. This provides a way of executing Rocq code efficiently and can be used to create verified software libraries.
Website: rocq-prover.org
Support: Documentation, GitHub Code Repository
Developer: INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2, Ascola, Galinette projects (starting 1985),- Laboratoire de l’Informatique du Parallelisme (LIP) associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997), Laboratoire de Recherche en Informatique (LRI) associated to CNRS and university Paris Sud (since Sep. 1997), Laboratoire d’Informatique de l’Ecole Polytechnique (LIX) associated to CNRS and Ecole Polytechnique (since Jan. 2003). Laboratoire PPS associated to CNRS and University Paris Diderot
License: GNU Lesser General Public License v2.1
Rocq Prover is written in OCaml. Learn OCaml with our recommended free books and free tutorials.
Related Software
| Proof Assistants | |
|---|---|
| Rocq Prover | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Lean | Programming language and theorem prover |
| Agda | Interactive system for writing and checking proofs |
| F* | Functional language for verified programs with dependent refinement types |
| HOL4 | Interactive higher-order logic environment for rigorous theorem development |
| Aya | Dependently typed language for formalisation and certified programming |
| Lambdapi | Logical framework for defining and checking expressive type systems |
| HOL Light | Lightweight higher-order logic system with a small trusted kernel |
| PVS | Specification and verification suite for analysing complex systems |
| LISA | Scala-based platform for formal mathematics and automated reasoning |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |
Please read our Comment Policy before commenting.