
Home page: http://coq.inria.fr
Coq is a formal proof management system. It provides a formal language for writing mathematical definitions, executable algorithms, and theorems with an IDE for semi-interactive development of machine-checked proofs. It is developed using the Objective Caml language (OCaml™, with a bit of C™. A complete reference manual, standard library, and other documents can be found on the Coq website. This is specialized software requiring a significant knowledge of formal mathematical theory, even if your intent is to develop or test software algorithms.