Coq Ecosystem
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.
Core Projects
MorePopular Projects
MoreUniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view
practical-fm
A gently curated list of companies using verification formal methods in industry
category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
Up and Coming Projects
More
software_foundations
platform-docs
A project of short tutorials and how-to guides for Coq features and Coq Platform packages
certpcspkr_linux
thesis
Master's Thesis in Computer Science: Verification of the Blocking and Non-Blocking Michael-Scott Queue Algorithms
trocq
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
mltt-consistency
Logical relation for predicative CC omega with booleans and an intensional identity type
software-foundations
Solutions (in Coq) of the exercises in the software foundation books
ACE-RISCV
Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for RISC-V with focus on a formally verified and auditable security monitor
metaprogramming-rosetta-stone
A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]
