Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

The CompCert formally-verified C compiler

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

《软件基础》中译版 Software Foundations Chinese Translation

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

An axiom-free formalization of category theory in Coq for personal study and practical work

Cosette is an automated SQL solver.

A framework for formally verifying distributed systems implementations in Coq

Mathematical Components

A port of Coq to Javascript -- Run Coq in your Browser

This repo is the new home of Proof General

Tricks you wish the Coq manual told you

A gently curated list of companies using verification formal methods in industry

Verified Software Toolchain

An introductory course to Homotopy Type Theory

Metaprogramming, verified meta-theory and implementation of Coq in Coq

A Coq IDE build on top of Proof General's Coq mode

A Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]

My personal repository of formally verified mathematics.