Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.
You can download the current stable version, Coq 8.5pl1, released in April 2016. Since version 8.5, Coq features among other things asynchronous edition of documents under CoqIDE, universe polymorphism, primitive projections, new extensions of the proof engine and a new reduction procedure by compilation to native code.