coq 话题在 GitHub 上没有填写简介，这里按 Star 数汇总最相关的热门仓库。
The Rocq Prover is an interactive theorem prover, or proof assistant. 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
Rust程序的验证工具链
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
《软件基础》中文版
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 是一个自动化的 SQL 求解器。
A framework for formally verifying distributed systems implementations in Coq
A gently curated list of companies using verification formal methods in industry
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
This repo is the new home of Proof General
Tricks you wish the Coq manual told you [maintainer=@tchajed]
A port of Coq to Javascript -- Run Coq in your Browser
Verified Software Toolchain
Visual Studio Code for Coq 扩展
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
高保证和高速密码学的语言
An introductory course to Homotopy Type Theory