Coq

Developed at INRIA starting in 1989, first released in 1991. An interactive theorem prover and dependently typed functional language. Used to formally verify mathematical proofs and critical software (CompCert C compiler). Renamed to Rocq in 2024.