Coq
Coq / Rocq proof assistant
Coq (recently rebranded as Rocq) is a formal proof management system and dependently typed functional language used to write and machine-verify mathematical proofs and to formally certify the correctness of software and hardware designs.
Definition
Coq (recently rebranded as Rocq) is a formal proof management system and dependently typed functional language used to write and machine-verify mathematical proofs and to formally certify the correctness of software and hardware designs.
Overview
Coq is one of the longest-established and most widely used interactive theorem provers, developed originally at INRIA in France. It combines a functional programming language, Gallina, with a tactic language used to interactively construct proofs step by step; each tactic invocation transforms the current proof goal until it is fully discharged, and Coq's kernel then mechanically checks that the resulting proof term is valid. Coq has been used for some of the most notable achievements in formally verified software and mathematics, including a fully machine-checked proof of the four-color theorem and CompCert, a C compiler whose functional correctness — that compiled code behaves according to the semantics of the source program — is formally proven in Coq rather than merely tested. This makes Coq particularly significant in domains where software bugs carry extreme cost, such as aerospace, cryptography, and compiler correctness. Coq's proof language and extensive tactic library give it a reputation for being powerful but with a steep learning curve, and it has an active academic and open-source community maintaining a large library of formalized mathematics (the Mathematical Components library, among others). It belongs to the same family of dependently typed proof assistants as Agda, Idris, and Lean, and remains a common reference point in formal methods research and industrial-strength verified software projects.
Key Features
- Interactive, tactic-based construction of machine-checked proofs
- Gallina functional programming language combined with a proof kernel
- Dependently typed foundation supporting precise formal specifications
- Used for landmark formal verification projects like CompCert and the four-color theorem proof
- Large ecosystem of formalized mathematics libraries
- Extraction of verified programs into languages like OCaml or Haskell
Use Cases
Alternatives
History
Coq — renamed "the Rocq Prover" in recent years — is an interactive theorem prover (proof assistant) for writing formal mathematical definitions, algorithms, and machine-checked proofs. It grew out of the Calculus of Constructions, first implemented in 1984 by Gérard Huet and Thierry Coquand at the French research institute INRIA. The system was released under the name Coq in 1989 and evolved to be based on the Calculus of Inductive Constructions. Coq became one of the most influential proof assistants in computer science, used for landmark formal-verification efforts such as the CompCert verified C compiler and a machine-checked proof of the Four Color Theorem, and as a teaching tool for formal methods.
Sources
- The Rocq Prover — early history of Coq (official docs) · as of 2026-07-17
- The Rocq Prover — official website · as of 2026-07-17