Rocq
In plain wordsA long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step.
An open-source proof assistantinteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong. based on the calculus of inductive constructions, a dependent type theory in which propositions are types and proofs are programs, so that checking a proof amounts to type-checking a term. Users write definitions and specifications in its functional language, Gallina, and build proofs interactively with tactics; a small kernel certifies them, and verified programs can be extracted to OCaml, Haskell or Scheme. Landmark achievements include formal proofs of the four color theorem and the Feit–Thompson odd order theorem (completed 2012) and the CompCert verified C compiler. Its corpora of formal proofs were among the first used to train machine-learning provers, and it remains a target for AI-generated verified code alongside LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs. and Isabelle.
Origin
Developed at INRIA in France from 1984, initiated by Thierry Coquand and Gérard Huet, with Christine Paulin-Mohring contributing inductive types; first released in 1989. A renaming announced in October 2023 took effect with Rocq 9.0 in March 2025; the name honors INRIA Rocquencourt and the mythical roc, keeping the old name's bird theme ('coq' is French for rooster).
Usage note
Its developers received the 2013 ACM Software System Award. Older papers, libraries and tools use the name Coq.
Related
- interactive theorem provinginteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong.
- LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way.
- autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify.
Sources
- Bertot, Y. & Castéran, P. (2004). Interactive Theorem Proving and Program Development — Coq'Art: The Calculus of Inductive Constructions. Springer.
- Leroy, X. (2009). Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 107–115.
Mentioned in
interactive theorem provinginteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong., LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs., autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify., IsabelleIsabelle, prop. n.: A widely used proof-checking program in which people write mathematics and verified software; it is known for automation that calls other theorem provers to finish routine steps., PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics.