This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

A framework for formally verifying distributed systems implementations in Coq

Verified Software Toolchain

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Formalization of C++ for verification purposes.

A foundational framework for modular cryptographic proofs in Coq

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Hahn: A Coq library

This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.

Partial Commutative Monoids

Formally verified Coq serialization library with support for extraction to OCaml

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

Coq utility and tactic library.

Sokoban (in Coq) [maintainer=@erikmd]

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

Binary rational numbers in Coq [maintainer=@herbelin]

Library of useful utility functions for Coq plugins

A Coq tactic for proving multivariate inequalities using SDP solvers