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. Typical

applications include the certification of properties of programming languages,

the formalization of mathematics and teaching.

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.

• UpdatedMar 19, 2025
• OCaml

The CompCert formally-verified C compiler

• UpdatedMar 18, 2025
• Coq

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

• UpdatedMar 17, 2025
• Coq

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

• UpdatedMar 14, 2022
• HTML

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

• UpdatedApr 1, 2024
• Coq

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications!✈️ 🚀 ⚕️ 🏦

• UpdatedMar 20, 2025
• Coq

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

• UpdatedJan 22, 2025
• Coq

Cosette is an automated SQL solver.

• UpdatedDec 18, 2024
• Lean

Mathematical Components

• UpdatedMar 19, 2025
• Coq

A framework for formally verifying distributed systems implementations in Coq

• UpdatedMay 17, 2024
• Coq

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

• UpdatedOct 24, 2024
• TypeScript

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

• UpdatedFeb 11, 2025

Tricks you wish the Coq manual told you [maintainer=@tchajed]

• UpdatedFeb 11, 2025
• Coq

This repo is the new home of Proof General

• UpdatedFeb 28, 2025
• Emacs Lisp

Verified Software Toolchain

• UpdatedMar 13, 2025
• Coq

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

• UpdatedMar 18, 2025
• Coq

Visual Studio Code extension for Coq

• UpdatedMar 10, 2025
• OCaml

An introductory course to Homotopy Type Theory

• UpdatedJul 24, 2020
• Agda

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

• UpdatedFeb 3, 2023
• Emacs Lisp

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

• UpdatedJan 2, 2025