8.12 bertsioa kaleratu da (albistea idazteko unean eskuragarri dagoen azken bertsio txikia 8.12.1 da) Coq (oilarra) teorema interaktiboa frogatzeko tresnarena.
Coq-ek Gallina (oilasko) menpeko programazio-lengoaia barne hartzen du, eraikuntza-kalkuluaren teorian oinarritzen dena.
Coq sistemak ordenagailuz egiazta daitezkeen teorema frogak eta programak garatzea ahalbidetzen du, zehaztapenarekin bat datozen frogak batera.
Bertsio berriak liburutegi estandarra eta dokumentazioa nabarmen hobetu ditu, eta hainbat errore ere konpondu ditu.
Iturria: linux.org.ru