Coq

Hoare Type Theoryimdea-software/htt

A verification system for reasoning about heap-manipulating programs using Separation logic embedded in Coq.

Hydras & Co.coq-community/hydra-battles

A Coq-based project exploring hydra battles, ordinal numbers, addition chains, and Gödel's incompleteness theorem through formalized mathematics.

Metalibplclub/metalib

A Coq library for mechanizing programming language metatheory with locally nameless representation of binders.

Infotheoaffeldt-aist/infotheo

A Rocq library for formal reasoning about discrete probabilities, information theory, and linear error-correcting codes.

CoqEALCoqEAL/CoqEAL

A Coq library for effective algebra, providing optimized algorithms and a refinement framework for changing data representations in proofs.

Mechanized Semanticsxavierleroy/cdf-mech-sem

Coq formalizations for a course on mechanized semantics, covering imperative/functional languages, compilers, static analysis, and program logics.

Name the Biggest Numbercodyroux/name-the-biggest-number

A Coq-based competition for formally proving the largest constructive number within computational constraints.

100 famous theorems proved using Coqcoq-community/coq-100-theorems

A collection of statements and proofs for 100 famous mathematical theorems formalized in the Coq proof assistant.

Q*certquerycert/qcert

A framework for developing and verifying domain-specific languages, with a focus on query, rules, and smart contract languages.

Unicoqunicoq/unicoq

A Coq plugin that replaces Coq's standard unification algorithm with an enhanced one supporting universe polymorphism and overloading.

Mtac2Mtac2/Mtac2

A typed tactic language plugin for Coq that enables backward reasoning with a monadic interface.

FCFadampetcher/fcf

A Coq framework for machine-checked proofs of cryptographic security in the computational model.

FreeSpeclthms/FreeSpec

A Coq framework for implementing, certifying, and executing impure computations with modular verification.

Relation Algebradamien-pous/relation-algebra

A modular relation algebra library for Rocq (Coq) with reflexive decision tactics for Kleene algebra with tests and related theories.

Waterproof proof languageimpermeable/coq-waterproof

A Coq plugin enabling proof writing in a natural, handwritten mathematical style to aid students in learning formal proof.

Finmapmath-comp/finmap

A Coq library extending Mathematical Components with finite sets, finite maps, and multisets on choicetypes.

Functional Algorithms Verified in SSReflectclayrat/fav-ssr

A Coq/SSReflect port of the 'Functional Algorithms Verified' book, formalizing functional data structures and algorithms.

Coq record updatetchajed/coq-record-update

A Coq library that automatically generates record update functions using typeclasses and Ltac2.

Regular Language Representationscoq-community/reglang

A Coq library providing verified translations between automata, regular expressions, and WS1S logic for regular languages.

Graph Theorycoq-community/graph-theory

A Coq library formalizing graph theory results, including Menger's Theorem, Hall's Marriage Theorem, and Wagner's Theorem.

Program Logicsxavierleroy/cdf-program-logics

Coq formalization of program logics (Hoare logic, separation logic, concurrent separation logic) for verifying imperative and concurrent programs.

CoqPrimethery/coqprime

A Coq library for certifying primality using Pocklington and Elliptic Curve certificates, with efficient modular arithmetic.

Paramcoqcoq-community/paramcoq

A deprecated Coq plugin for generating parametricity statements and proofs from Coq definitions.

Waterproof editorimpermeable/waterproof

An educational environment for writing mathematical proofs in interactive notebooks, now available as a VS Code extension.

TLCcharguer/tlc

A general-purpose Coq library providing an alternative to Coq's standard library with extensionality axioms and enhanced tactics.

Algebra Tacticsmath-comp/algebra-tactics

Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.

Odd Order Theoremmath-comp/odd-order

A formal verification of the Feit-Thompson theorem (Odd Order Theorem) using the Coq proof assistant and Mathematical Components library.

AAC Tacticscoq-community/aac-tactics

A Coq plugin providing tactics for rewriting universally quantified equations modulo associativity and commutativity.

CoLoRfblanqui/color

A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.

FCSL-PCMimdea-software/fcsl-pcm

A Coq library formalizing Partial Commutative Monoids (PCMs) for separation logic-based program verification.

Simple IOLysxia/coq-simple-io

A library providing a purely functional IO monad for Coq, enabling direct implementation of IO programs with OCaml bindings.

lngenplclub/lngen

Generates locally nameless definitions and infrastructure lemmas for Coq from Ott language specifications.

Mczifymath-comp/mczify

Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.

mCoqEngineeringSoftware/mcoq

Mutation analysis tool for Coq verification projects to detect incomplete specifications.

Gaiacoq-community/gaia

A Coq formalization of Bourbaki's Elements of Mathematics, covering set theory and number theory using the Mathematical Components library.

Bedrock Bit Vectorsmit-plv/bbv

A unified Coq library for bit vectors used across multiple MIT research projects.