Version 8.12 has been released (the latest available minor version at the time of writing the news is 8.12.1) of the interactive theorem proving tool Coq (cockerel).
Coq includes the Gallina (chicken) dependent type programming language, which is based on the theory of construct calculus.
The Coq system allows you to develop both computer-verifiable theorem proofs and programs along with proof of conformance to the specification.
The new version has significantly improved the standard library and documentation, and also fixed a number of errors.
Source: linux.org.ru