Rocq

Tools: Rocq (formerly Coq)

• (Formal system, Language feature/design, Proof/Reason technique) An interactive theorem prover (formerly Coq) that enables formal verification of mathematical proofs and program correctness, using Dependent types and the Calculus of inductive construction.

• Name history

  Formerly Coq (after Thierry Coquand + CoC abbreviation + the French rooster symbolizing pride), renamed Rocq in 2024 (honoring Rocquencourt, Inria's founding site, and evoking the roc, a mythical bird of strength).