Coq is a formal system for proof management. It is a formal language for writing mathematical definitions, executable algorithms, and theorems. It also provides an environment for semi-interactive design of machine-checked proves.
Download Coq For MAC
Whats New
Version 8.9.1:
Main changes:
Some quality-of-life bug fixes
Many improvements to the documentation
A critical bug fix related to primitive projections and native_compute
Several additional Coq libraries shipped with the Windows installer