Top 23 coq Open-Source Projects

  • coq

    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.

    Project mention: Rosenpass – formally verified post-quantum WireGuard | | 2023-02-28
  • CompCert

    The CompCert formally-verified C compiler

    Project mention: Rosenpass – formally verified post-quantum WireGuard | | 2023-02-28
  • SonarLint

    Clean code begins in your IDE with SonarLint. Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today.

  • magmide

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

    Project mention: Announcing Magmide Month! (proof language for/using Rust) | | 2023-02-28
  • jscoq

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

  • practical-fm

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

    Project mention: We Need Simpler Types (speculations on what can be improved in future type systems and on erasing the boundaries between types and values) | | 2022-09-14 Look for Coq, Agda, Idris, MS - F*.

  • proofs

    My personal repository of formally verified mathematics.

    Project mention: Thoughts on proof assistants? | | 2022-12-13

    Personally I treat Coq like an extension of my brain. Whenever I'm uncertain about something, I formalize it in Coq. I have a repository of proofs with GitHub Actions set up in such a way forbids me from pushing commits containing mathematical mistakes. I've formalized various aspects of category theory, type theory, domain theory, etc., and I've also verified a few programs, such as this sorting algorithm. Lately I've been experimenting with a few novel types of graphs, proving various properties about them with the aim of eventually developing a way to organize all of my data (files, notes, photos, passwords, etc.) in some kind of graph structure like that.

  • awesome-coq

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

    Project mention: Coq is one of the most fun and enjoyable programming languages I ever use. | | 2023-03-13

    Coq has an awesome list by the community:

  • InfluxDB

    Access the most powerful time series database as a service. Ingest, store, & analyze all types of time series data in a fully-managed, purpose-built database. Keep data forever with low-cost storage and superior data compression.

  • Coqtail

    Interactive Coq Proofs in Vim

    Project mention: Code completion for Coq. | | 2022-09-05

    I've looked at both of these before, but neither of them fit the bill. Both are used for interactive execution of Coq programs from inside Neovim (I already use for that purpose), but neither provides code completion. Nonetheless, thank you so much for your help. Much appreciated.

  • coq-of-ocaml

    Formal verification for OCaml

    Project mention: What is a really cool thing you would want to write in Rust but don't have enough time, energy or bravery for? | | 2022-06-08

    Coq of OCaml is a good example of how I want it to be for rust

  • Coq-Equations

    A function definition package for Coq

  • principia

    The Principia Rewrite (by LogicalAtomist)

    Project mention: Principia Mathematica in modern notation. | | 2022-07-21

    You can check it out here:

  • verdi-raft

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

  • jasmin

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

    Project mention: Let's collect relatively new research programming languages in this thread | | 2022-11-15

    Jasmin, late 2010s, a language designed to be lower-level than C and provide good low-level control for cryptographic code. Basically a new take on "C as a high-level assembly language", with formal semantics etc. I suspect that this design space is rather close to "a good language to use as a compiler backend", but I think this would require changes to Jasmin and no one is working on that as far as I know.

  • fourcolor

    Formal proof of the Four Color Theorem [[email protected]]

  • kami

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

  • ttlite

    A SuperCompiler for Martin-Löf's Type Theory

  • coq-serapi

    Coq Protocol Playground with Se(xp)rialization of Internal Structures.

  • corn

    Coq Repository at Nijmegen [[email protected],@VincentSe]

  • toychain

    A minimalistic blockchain consensus implemented and verified in Coq

  • koika

    A core language for rule-based hardware design 🦑

    Project mention: Let's collect relatively new research programming languages in this thread | | 2022-11-15 Algebraic effects and reference counting. hardware description DSL for coq

  • coq-library-undecidability

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

    Project mention: Development Environment with guix shell for Coq Package | | 2022-08-21

    I want to run guix shell to create an environment with the dependencies required to build coq-library-undecidability.

  • next-700-module-systems

    PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

  • vericert

    A formally verified high-level synthesis tool based on CompCert and written 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-03-13.

coq related posts


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

Project Stars
1 coq 4,128
2 CompCert 1,571
3 magmide 750
4 jscoq 471
5 practical-fm 412
6 proofs 240
7 awesome-coq 215
8 Coqtail 205
9 coq-of-ocaml 202
10 Coq-Equations 195
11 principia 190
12 verdi-raft 165
13 jasmin 146
14 fourcolor 124
15 kami 122
16 ttlite 112
17 coq-serapi 109
18 corn 106
19 toychain 103
20 koika 102
21 coq-library-undecidability 93
22 next-700-module-systems 72
23 vericert 69
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives