Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
Compiler Backend for LSTS (Typed Macro Assembler)
Trust infrastructure for AI agents. Know who produced a value, when, and that it hasn't been tampered with. Zero dependencies. Pure C.
Misc playground and random stuff
Post-Quantum Cryptographic primitives and Mechanized Proofs (Patent Pending)
Formally verified programming language with security properties proven in Coq. Zero external dependencies. Thousands theorems. 0 admits.
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989