The CompCert formally-verified C compiler

A Coq library for Homotopy Type Theory

Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

This rocq 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

FSCQ is a certified file system written and proven in Coq

Voevodsky's original development of the univalent foundations of mathematics in Coq

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

Cuq: A MIR-to-Coq Framework Targeting PTX for Formal Semantics and Verified Translation of Rust GPU Kernels

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

PeaCoq is a pretty Coq, isn't it?

A formalization of category theory in the Coq proof assistant.

A web server written in Coq.

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

Coq library for verified low-level programming

Distributed Data Structures in Coq

a capability-based system

A framework for extensible, reflective decision procedures.

A formalization of synthetic differential geometry in Coq using infinitesimal analysis

Formalisation of Operational Transformation in Coq

Reflective verification procedures for separation logic programs in Coq

Certified Relational to Imperative

Port of Bedrock to use MirrorShard library for computational reflection

Convenience functions for unit testing in Coq.

Harvard's Ynot: http://ynot.cs.harvard.edu/ - One branch per Coq version which needed changes

Alias analysis for CompCert