
Домашня сторінка: http://coq.inria.fr
Coq — система керування формальними доведеннями. Використовує формальну мову для запису математичних визначень, виконуваних алгоритмів та теорем та IDE для напівінтерактивної розробки доведень з комп’ютерною перевіркою. Розроблено з використанням Objective Caml та Camlp5. На сайті Coq можна знайти повний довідник, стандартну бібліотеку та іншу документацію. Це високоспеціалізоване програмне забезпечення, яке потребує значних знань формальної математичної теорії, навіть якщо вашою метою є розробка або тестування алгоритмів роботи програмного забезпечення.