Coq

Homotopy Type TheoryHoTT/Coq-HoTT

A Coq library for formalizing Homotopy Type Theory, interpreting type theory into homotopy theory.

UniMathUniMath/UniMath

A Coq library formalizing mathematics using univalent foundations and homotopy type theory.

Sailrems-project/sail

A language for formally specifying instruction-set architecture (ISA) semantics with tooling for emulators, documentation, and verification.

Fiat-Cryptomit-plv/fiat-crypto

Synthesizes formally verified, correct-by-construction C, Rust, Go, and other language code for cryptographic field arithmetic primitives.

Category Theory in Coqjwiegley/category-theory

An axiom-free formalization of category theory in Coq for representation, manipulation, and realization of categorical terms.

Verdiuwplse/verdi

A Coq framework for implementing and formally verifying distributed systems with support for multiple fault models.

Tricks in Coqcoq-community/coq-tricks

A collection of hard-to-discover tips, tricks, and features for the Coq proof assistant.

QuickChickQuickChick/QuickChick

A randomized property-based testing plugin for Coq, enabling automated test generation and verification within proof assistants.

coq-of-ocamlformal-land/coq-of-ocaml

Translates OCaml programs to Coq for formal verification of properties like invariants, absence of failures, and backward compatibility.

CoqOfOCamlclarus/coq-of-ocaml

Translates OCaml programs to Coq for formal verification of properties like invariants and absence of failures.

Interaction TreesDeepSpec/InteractionTrees

A Coq library for representing and reasoning about recursive, effectful, and non-terminating programs using interaction trees.

Four Color Theoremcoq-community/fourcolor

A formal proof of the Four Color Theorem in Coq, including supporting theories for real numbers, plane topology, and combinatorial hypermaps.

Analysismath-comp/analysis

A formal real analysis library for the Coq/Rocq proof assistant, built on the Mathematical Components library.

Equationsmattam82/Coq-Equations

A function definition plugin for Rocq/Coq that provides notation for dependent pattern-matching and well-founded recursion.

GeoCoqGeoCoq/GeoCoq

A formalization of geometry in Coq based on Tarski's axiom system, containing both foundational and high-school style proofs.

Verdi Raftuwplse/verdi-raft

A formally verified implementation of the Raft distributed consensus protocol in Coq using the Verdi framework.

Coq-ElpiLPCIC/coq-elpi

A Coq plugin that embeds the Elpi λProlog interpreter to define new commands and tactics for theorem proving.

CertiCoqCertiCoq/certicoq

A verified compiler for Gallina (Rocq Prover's specification language) that targets WebAssembly and Clight.

coq-haskelljwiegley/coq-haskell

A Coq library providing Haskell-like definitions and notations for formalizing Haskell types and functions in Coq.

SMTCoqsmtcoq/smtcoq

A Coq plugin that checks proof witnesses from external SAT/SMT solvers and provides certified decision procedures.

Math Classescoq-community/math-classes

A Coq library providing abstract interfaces for mathematical structures using type classes.

Lectures on Software Foundationsclarksmr/sf-lectures

Lecture materials and Coq source files accompanying YouTube videos on the Software Foundations textbook.

Fiatmit-plv/fiat

A Coq library for deductive synthesis of correct-by-construction abstract data types and parsers.

Formalised Undecidable Problemsuds-psl/coq-library-undecidability

A Coq library containing mechanized reductions to establish undecidability results for problems in logic and computation.

ExtLibcoq-community/coq-ext-lib

A library of Coq definitions, theorems, and tactics for use in other Coq developments.

Coq'Art Exercises and Tutorialscoq-community/coq-art

Coq code and solutions for exercises from the Coq'Art book, a foundational text on the Coq proof assistant.

ConCertAU-COBRA/ConCert

A Coq framework for formal verification, property-based testing, and extraction of smart contracts.

Ceramistcertichain/ceramist

A Coq library for formally verifying probabilistic properties of hash-based approximate membership query structures like Bloom filters.

WasmCert-CoqWasmCert/WasmCert-Coq

A mechanized formalization of WebAssembly 2.0 in Coq (Rocq) with soundness proofs and an extracted interpreter.

RISC-V Specification in Coqmit-plv/riscv-coq

A formal specification of the RISC-V instruction set architectures (RV32I, RV64I) and extensions (A, M) written in the Coq proof assistant.

CoRNcoq-community/corn

A Coq library for constructive real analysis and algebra, including a model of real numbers and exact real computation.

Hierarchy Buildermath-comp/hierarchy-builder

A Coq plugin providing high-level commands to declare and manage hierarchies of algebraic structures using packed classes.

coq-dpdgraphcoq-community/coq-dpdgraph

A Coq plugin that extracts dependency graphs between Coq objects and provides tools for visualization and analysis.

hs-to-coqplclub/hs-to-coq

A tool that converts Haskell source code into equivalent Coq source code for formal verification.

Jupyter kernel for CoqEugeneLoy/coq_jupyter

A Jupyter kernel for the Coq proof assistant, enabling interactive theorem proving in notebooks.

SSProveSSProve/ssprove

A foundational framework for modular cryptographic proofs in the Coq proof assistant, enabling state-separating proofs.