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 www.getonboard.dev. Learn more →
Top 23 Coq coq Projects

Project mention: Can the language of proof assistants be used for general purpose programming?  news.ycombinator.com  20231027
Also a C compiler (https://compcert.org/). I did exaggerate bit in saying that anything nontrivial 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.
For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:
UniMath (https://github.com/UniMath/UniMath, mentioned in the article)
CoqHoTT (https://github.com/HoTT/CoqHoTT)
agdaunimath (https://unimath.github.io/agdaunimath/)
cubical agda (https://github.com/agda/cubical)
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 www.getonboard.dev.

magmide
A dependentlytyped 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  20230704https://github.com/magmide/magmide when

Project mention: Which proof assistant is the best to formalize real analysis/probability/statistics?  /r/Coq  20230618

Project mention: A Taste of Coq and Correct Code by Construction  news.ycombinator.com  20230903
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: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
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!



InfluxDB
Collect and Analyze Billions of Data Points in Real Time. Manage all types of time series data in a single, purposebuilt database. Run at any scale in any environment in the cloud, onpremises, or at the edge.

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

Project mention: Which proof assistant is the best to formalize real analysis/probability/statistics?  /r/Coq  20230618

Takes around 15 minutes on my machine.
[0] https://github.com/coqcommunity/fourcolor
[1] https://github.com/NixOS/nixpkgs/blob/master/pkgs/developmen...

kami
A Platform for HighLevel Parametric Hardware Specification and its Modular Verification (by mitplv)




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





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 selfcontained, and is thus "pure".


regexpBrzozowski
Coq formalization of decision procedures for regular expression equivalence [maintainer=@antontrunov]
Project mention: Show HN: Regex Derivatives (Brzozowski Derivatives)  news.ycombinator.com  20230307Thanks for sharing. I am not familiar with Agda. Will take a look. There is somewhat similar code in COQ: https://github.com/coqcommunity/regexpBrzozowski


SaaSHub
SaaSHub  Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Coq coq related posts
 Can the language of proof assistants be used for general purpose programming?
 A Taste of Coq and Correct Code by Construction
 Will Computers Redefine the Roots of Math?
 Recently I am having too much friction with the borrow checker... Would you recommend I rewrite the compiler in another language, or keep trying to implement it in rust?
 Inspiring OOP examples?
 There is such thing called bugfree code.
 Proofs about Programs

A note from our sponsor  Onboard AI
getonboard.dev  3 Dec 2023
Index
What are some of the best opensource coq projects in Coq? This list will help you:
Project  Stars  

1  CompCert  1,695 
2  UniMath  876 
3  magmide  784 
4  mathcomp  515 
5  proofs  276 
6  CoqEquations  205 
7  jasmin  189 
8  verdiraft  175 
9  analysis  167 
10  fourcolor  138 
11  kami  132 
12  koika  116 
13  toychain  108 
14  corn  108 
15  coqlibraryundecidability  98 
16  ConCert  98 
17  vericert  71 
18  hstocoq  71 
19  rupicola  46 
20  coqsimpleio  27 
21  aneris  27 
22  regexpBrzozowski  12 
23  doublygeneric  4 