Coq coq

Open-source Coq projects categorized as coq

Top 23 Coq coq Projects

  • CompCert

    The CompCert formally-verified C compiler

    Project mention: Can the language of proof assistants be used for general purpose programming? | | 2023-10-27

    Also a C compiler ( I did exaggerate bit in saying that anything non-trivial is "nearly impossible".

    However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.

  • UniMath

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

    Project mention: Will Computers Redefine the Roots of Math? | | 2023-06-30

    For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:

    UniMath (, mentioned in the article)

    Coq-HoTT (

    agda-unimath (

    cubical agda (

    All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).

  • Onboard AI

    Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at

  • magmide

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

    Project mention: Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think? | /r/rust | 2023-07-04 when

  • math-comp

    Mathematical Components

    Project mention: Which proof assistant is the best to formalize real analysis/probability/statistics? | /r/Coq | 2023-06-18
  • proofs

    My personal repository of formally verified mathematics.

    Project mention: A Taste of Coq and Correct Code by Construction | | 2023-09-03

    If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here:

    My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you've heard about proof assistants like Coq or Lean and you're fascinated by what they can do, and you just want the TL;DR of how they work, then this tutorial is written for you.

    Any feedback is appreciated!

  • Coq-Equations

    A function definition package for Coq

  • jasmin

    Language for high-assurance and high-speed cryptography (by jasmin-lang)

  • InfluxDB

    Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purpose-built database. Run at any scale in any environment in the cloud, on-premises, or at the edge.

  • verdi-raft

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

  • analysis

    Mathematical Components compliant Analysis Library (by math-comp)

    Project mention: Which proof assistant is the best to formalize real analysis/probability/statistics? | /r/Coq | 2023-06-18
  • fourcolor

    Formal proof of the Four Color Theorem [maintainer=@ybertot]

    Project mention: On the Four Color Problem | | 2023-04-07

    Takes around 15 minutes on my machine.



  • kami

    A Platform for High-Level Parametric Hardware Specification and its Modular Verification (by mit-plv)

  • koika

    A core language for rule-based hardware design 🦑

  • toychain

    A minimalistic blockchain consensus implemented and verified in Coq

  • corn

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

  • coq-library-undecidability

    A library of mechanised undecidability proofs in the Coq proof assistant.

  • ConCert

    A framework for smart contract verification in Coq

  • vericert

    A formally verified high-level synthesis tool based on CompCert and written in Coq.

  • hs-to-coq

    Convert Haskell source code to Coq source code.

  • rupicola

    Gallina to Bedrock2 compilation toolkit

  • coq-simple-io

    IO for Gallina

    Project mention: Inspiring OOP examples? | /r/java | 2023-03-12

    My point about a proof assistant language, let's just say Coq, is focused on pure, referentially transparent functions. There are no IORef like escape hatches required to make things work, although you could probably argue that stuff like this is still pure as, there are certainly escape hatches. Generally speaking, in proof assistants, the program can be self-contained, and is thus "pure".

  • aneris

    Program logic for developing and verifying distributed systems

  • regexp-Brzozowski

    Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

    Project mention: Show HN: Regex Derivatives (Brzozowski Derivatives) | | 2023-03-07

    Thanks for sharing. I am not familiar with Agda. Will take a look. There is somewhat similar code in COQ:

  • doubly-generic

    Arity-generic datatype-generic, or doubly-generic, programming in Coq.

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020). The latest post mention was on 2023-10-27.

Coq coq related posts


What are some of the best open-source coq projects in Coq? This list will help you:

Project Stars
1 CompCert 1,695
2 UniMath 876
3 magmide 784
4 math-comp 515
5 proofs 276
6 Coq-Equations 205
7 jasmin 189
8 verdi-raft 175
9 analysis 167
10 fourcolor 138
11 kami 132
12 koika 116
13 toychain 108
14 corn 108
15 coq-library-undecidability 98
16 ConCert 98
17 vericert 71
18 hs-to-coq 71
19 rupicola 46
20 coq-simple-io 27
21 aneris 27
22 regexp-Brzozowski 12
23 doubly-generic 4
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives