
Home Page: http://coq.inria.fr
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an IDE for semi-interactive development of machine-checked proofs. It is developed using Objective Caml and Camlp5. A complete reference manual, standard library and other documents are found on it the Coq website. This is specialised software requiring a significant knowledge of formal mathematical theory even if your intent is to develop or test software algorithms.