Ang bersyon 8.12 ay inilabas (ang pinakabagong magagamit na menor de edad na bersyon sa oras ng pagsulat ng balita ay 8.12.1) ng interactive na theorem na nagpapatunay na tool na Coq (cockerel).
Kasama sa Coq ang Gallina (chicken) dependent type programming language, na batay sa teorya ng construct calculus.
Ang Coq system ay nagbibigay-daan sa iyo na bumuo ng parehong computer-verify na theorem proofs at mga programa kasama ang patunay ng pagsunod sa mga detalye.
Ang bagong bersyon ay makabuluhang napabuti ang karaniwang library at dokumentasyon, at naayos din ang ilang mga error.
Pinagmulan: linux.org.ru