Welcome to a World of Rocq
A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.
Rocq's highly expressive type system and proof language enable fully mechanised verification of programs with respect to strong specifications in a wide variety of languages. Through the Curry-Howard lens, it simultaneously provides a rich logic and foundational computational theory for mathematical developments, supported by a flexible proof environment. Its well-studied core type theory, resulting from over 40 years of research, is implemented in a well-delimited kernel using the performant and safe OCaml programming language, providing the highest possible guarantees on mechanised artifacts. The core type theory is itself formalised in Rocq in the MetaRocq project, a verified reference checker is proven correct and complete with respect to this specification and can be extracted to reduce the trusted code base of any formalization to the specification of Rocq's theory and the user specification.
The Rocq Prover enables a very wide variety of developments to coexist in the same system, ranging from end-to-end verified software and hardware models to the development of higher-dimensional mathematics. Flagship projects using Rocq include the Mathematical Components library and its derived proofs of the Four-Color and Feith-Thompson theorems; the verified CompCert C compiler and the associated Verified Software Toolchain for proofs of C-like programs, or the development of Homotopy Type Theory and Univalent Foundations of mathematics. Rocq is also a great vehicle for teaching logic and computer science as exemplified by the thousands of students that have gone through the Software Foundations series of books. Rocq's development is entirely open-source and a large and diverse community of users participate in its continued evolution.
