OPAM

ALEAcoq-community/alea

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

Stable sort algorithms in Coqpi8027/stablesort

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

Coqobancoq-community/coqoban

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

CertiGraphSalamari/CertiGraph

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

Tarjan and Kosarajumath-comp/tarjan

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

ValidateAxot017/validate

An OCaml library that uses a PPX deriver to automatically generate validators for records, variants, lists, and values via annotations.

Coqtail Mathcoq-community/coqtail-math

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

MathComp Tutorial Materialsmath-comp/tutorial_material

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

OCaml OpenFlowfrenetic-lang/ocaml-openflow

OCaml library for serializing and deserializing OpenFlow protocol messages, supporting versions 1.0 and 1.3.

RunOrgRunOrg/RunOrg

An open-source social database server built with OCaml and PostgreSQL for managing user profiles and relationships.

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.

OCaml@ptsubame-sp/ocaml_at_p

A debugging printer for OCaml that automatically generates print functions and inserts debug output for expressions marked with [@p].

CryptOSSrvantonder/CryptOSS

Tooling for collecting and analyzing cryptocurrency open-source software development activity from GitHub.

MathComp Schoolgares/math-comp-school-2022

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

Docker-MathCompmath-comp/docker-mathcomp

Docker images providing stable versions of the Mathematical Components library for the Coq proof assistant.