Coq

Hahnvafeiadis/hahn

A Coq library providing lemmas and tactics for reasoning about lists and binary relations.

Lemma Overloadingcoq-community/lemma-overloading

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq's Hoare Type Theory.

Hanoithery/hanoi

A formal Coq development of the Tower of Hanoi problem with generalized frameworks and proofs.

ALEAcoq-community/alea

A Coq library for formal verification of randomized algorithms using a monadic probability distribution interpretation.

Coinductiondamien-pous/coinduction

A Coq library providing enhanced coinductive proof methods based on the 'companion' concept from coinduction theory.

Stable sort algorithms in Coqpi8027/stablesort

A Rocq library providing stable mergesort algorithms with formal correctness proofs using relational parametricity.

Bignumscoq/bignums

A Coq library providing arbitrarily large integer and rational numbers (BigN, BigZ, BigQ) for formal verification.

Coqobancoq-community/coqoban

A Coq implementation of Sokoban, the Japanese warehouse keeper puzzle game.

LibHypsMatafou/LibHyps

A Coq library providing tactics and tacticals for hypothesis manipulation during proofs.

T2048thery/T2048

A formal verification of the 2048 game implemented in the Coq proof assistant.

RoosterizeEngineeringSoftware/roosterize

A neural network-based tool that suggests lemma names for Coq verification projects by analyzing serialized statements and elaborated terms.

CertiGraphSalamari/CertiGraph

A Coq library for formal verification of graph-manipulating C programs, compatible with CompCert and VST.

Autosubst-ocamluds-psl/autosubst-ocaml

Generates Coq boilerplate code for handling binders, renaming, and substitutions in formal language metatheory.

Sudokucoq-community/sudoku

A certified Sudoku solver implemented in Coq using a formalized Davis-Putnam procedure.

Tarjan and Kosarajumath-comp/tarjan

Coq formalization and correctness proofs of Tarjan's and Kosaraju's algorithms for finding strongly connected components in graphs.

TraktecranceMERCE/trakt

A generic goal preprocessing tool for proof automation tactics in Coq.

MathComp Tutorial Materialsmath-comp/tutorial_material

Proof scripts and materials for tutorials on the Mathematical Components library and small-scale reflection in Coq.

Coqtail Mathcoq-community/coqtail-math

A Coq library of formally verified mathematical theorems and tools covering arithmetic, real analysis, and complex analysis.

Completeness and Decidability of Modal Logic Calculicoq-community/comp-dec-modal

Machine-checked constructive proofs of soundness, completeness, and decidability for modal logics K, K*, CTL, and PDL.

Floating-Point Numbers and Formal Proofthery/FlocqLecture

An introductory course on formal verification of floating-point numbers and real numbers using the Coq proof assistant and Flocq library.

Natural Number Gameuncomputable/natural-number-game

A Coq reimplementation of the Natural Number Game, providing interactive theorem proving exercises for learning mathematical proofs.

MathComp Schoolgares/math-comp-school-2022

Coq lessons and exercises introducing the SSReflect proof language and Mathematical Components library.

MathComp Extrathery/mathcomp-extra

A collection of formalized mathematical theories and algorithms extending the Mathematical Components library for Coq.

Mini-Rubikthery/minirubik

A certified solver for the 2x2 Rubik's Cube, formally verified in Coq.

Coq-KruskalDmxLarchey/Coq-Kruskal

A modular Coq library providing constructive, axiom-free proofs of Kruskal's Tree Theorem and related results using almost full relations.