Coq

Coq — это система интерактивного доказательства теорем, в которой используется собственный функциональный язык программирования с зависимыми типами — Gallina, а также различные мета-языки тактик, описывающих как строить программы на Gallina, представляющие формальные доказательства. Его разработку начали ещё в середине 80-х годов сотрудники ведущего французского института INRIA. Coq позволяет записывать и автоматически проверять предельно строгие доказательства чистых математических теорем, а также верифицировать корректность программных систем, таких как компиляторы и операционные системы/гипервизоры виртуальных машин, разрабатываемые индустриальными стартапами (Bedrock Systems, Formal Vindications), использующими формальную верификацию как конкурентное преимущество.