Coq

Coq 係一隻交互式嘅定理證明輔助工具。佢允許用家輸入包含數學斷言嘅表達式、機械化咁對呢啲斷言執行檢查、幫助構造形式嘅證明、仲可以由佢形式化描述嘅構造性證明入面提取到可驗證嘅程序。