Top 14 coq Open-Source Projects

  • GitHub repo 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: Which Prof for 191? | | 2021-10-06
  • GitHub repo CompCert

    The CompCert formally-verified C compiler

    Project mention: Multicore OCaml: September 2021, effect handlers will be in OCaml 5.0 | | 2021-10-04

    OCaml is becoming a must learn language for those who want to take their C programming to the highest levels, because:

    1. Frama-C, which enables writing bug-free C programs, is implemented using a combination of OCaml and the Coq proof assistant (which is itself implemented in OCaml):

    2. CompCert, a formally verified C compiler, is implemented using OCaml and Coq:

    Nothing at this level yet exists in the Rust and Zig ecosystems, for example. Rust is a very complicated language with many features which makes formalization much harder than with C and OCaml, which both had mathematical ideas of simplicity, analyzability, and minimalism inspire their designs, even if they continue to grow into more complicated monsters, which, incidentally this OCaml 5.0 release will contribute towards. :-)

  • Scout APM

    Scout APM: A developer's best friend. Try free for 14-days. Scout APM uses tracing logic that ties bottlenecks to source code so you know the exact line of code causing performance issues and can get back to building a great product faster.

  • GitHub repo jscoq

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

    Project mention: Online theorem provers | | 2021-08-24

    I have found some instances of jsCoq but nothing else. Do you know some other online platform? (Whatever the underlying prover or logic)

  • GitHub repo practical-fm

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

    Project mention: A list of companies that use formal verification methods | | 2021-02-08
  • GitHub repo Coq-Equations

    A function definition package for Coq

    Project mention: Learn coq or agda before diving into idris2? | | 2021-05-02

    I'd say Agda is more similar to Idris than Coq. Coq has a different syntax and isn't as good for programming with dependent types as Agda and Idris (Agda and Idris both put a huge emphasis on dependent pattern matching, something that Coq only recently gained support for through the Equations package).

  • GitHub repo Coqtail

    Interactive Coq Proofs in Vim

    Project mention: Is MATH145 worth it? | | 2021-09-15

    If you're finding coqide hard to use, I used to use coquille back in the day so that I didn't have to lose my neovim workflow (though it seems like coqtail is the currently maintained fork). I remember djao himself used to use proof general with emacs, which looks like another nice option if you're an emacs user.

  • GitHub repo coq-serapi

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

    Project mention: Translating My Z3 Tutorial to Coq | | 2021-02-27

    It's a question I hadn't really considered before. On first pass, as far as I know, I'd say the answer is no. It isn't clear to me what the objective of embedding Coq with a C api for example would be. The very core of Coq is about verifying proofs and not producing them and I'm not sure what the benefit of embedding it is.

    Having said that there are a few projects that may be something like what you're asking. First off, Coq has the SerAPI project through which external programs can talk to coq. This has been used for example to make a python OpenAi gym like interface

    A different direction might be something like MetaMath Zero which is intended to be a small and fast verifier for it's language, perhaps maybe someday for embedding in applications. There is this notion of "Proof Carrying Code" which I don't really know what the current state of the art is. One might want an easily embeddable trusted verifier for that purpose. I don't know.

  • Nanos

    Run Linux Software Faster and Safer than Linux with Unikernels.

  • GitHub repo corn

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

    Project mention: The Fundamental Theorem of Algebra in ACL2 | | 2021-07-29

    > Or there are these high level systems for proving deep theorems. Is anyone trying to fill the gap?

    There's ongoing work on computable real numbers for instance the CoRN library[1], so hope is on the horizon, for instance, a recent update to the Coq Interval package adds certified plotting, that is, the library guarantees that if a function passes through a pixel, that pixel is filled[2]. There's also the user-friendly Coquelicot[3] real analysis library up to basic differential equations (e.g. Bessel function).

    > It'll rearrange an equation but I can't ask it "prove this is increasing"

    For a taste, here's my proof that the cube function is increasing[4]. If I wanted to create a tactic that automatically proves a function is increasing, I would use properties of increasing functions[5] to recursively break it down into trivial subcases.







  • GitHub repo fourcolor

    Formal proof of the Four Color Theorem

    Project mention: Solution to the four color theorem in haskell | | 2021-05-27
  • GitHub repo toychain

    A minimalistic blockchain consensus implemented and verified in Coq

    Project mention: A minimalistic blockchain consensus implemented and verified in Coq | | 2021-03-04
  • GitHub repo silveroak

    Formal specification and verification of hardware, especially for security and privacy.

    Project mention: Silveroak - Formal specification and verification of hardware | | 2021-05-20
  • GitHub repo 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.

    Project mention: The Next 700 Module Systems [pdf] | | 2021-05-23
  • GitHub repo coq-library-undecidability

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

    Project mention: Math proof databases | | 2021-04-14

    There are two problems. The first is that there is no central repository. Sure, maybe if you're interested in undecidable results you might go here... But it's an island, and so is every other library. Worse yet, there's little inter mixing or combinable ways to use libraries. Unlike other programming languages, automated proof systems have so far been aimed at the technical aspects of a single person proving something, rather than the shareability of proofs.

  • GitHub repo coq_wordpress

    COQ.nvim support for WordPress hooks

    Project mention: popui.nvim - GUI popfix per codeAction (e forse anche altro) | | 2021-10-10

    PS: io ho solo fatto un plugin per Coq e i meiie dotfiles

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 2021-10-10.


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

Project Stars
1 coq 3,483
2 CompCert 1,308
3 jscoq 413
4 practical-fm 320
5 Coq-Equations 166
6 Coqtail 131
7 coq-serapi 100
8 corn 99
9 fourcolor 99
10 toychain 95
11 silveroak 90
12 next-700-module-systems 69
13 coq-library-undecidability 65
14 coq_wordpress 3
Find remote jobs at our new job board There are 34 new remote jobs listed recently.
Are you hiring? Post a new remote job listing for free.
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives