Coq topic
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.
Coq-Equations
A function definition package for Coq
principia
The Principia Rewrite
coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
coq-of-ocaml
Formal verification for OCaml
awesome-coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
awesome-provable
A curated set of links to formal methods involving provable code.
math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]