Coq
Interactive proof assistant based on the Calculus of Constructions — used to formally verify compiler correctness and mathematical theorems.
static
compiled
since 1989
functionaldependent-types
Coq is one of the most widely used proof assistants in computer science. The CompCert formally verified C compiler was proved correct in Coq, as was the seL4 microkernel. Coq proofs are checked by a small trusted kernel, making it applicable to safety-critical certification. Coq is now renamed Rocq following a 2024 community decision.