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.

SSProveSSProve/ssprove

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

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.

Unicoqunicoq/unicoq

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

Q*certquerycert/qcert

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

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.

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.

Waterproof proof languageimpermeable/coq-waterproof

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

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.

Paramcoqcoq-community/paramcoq

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

CoqPrimethery/coqprime

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

Waterproof editorimpermeable/waterproof

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