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. Learn more →
Top 23 coq OpenSource 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 semiinteractive development of machinechecked proofs.
Project mention: Rosenpass – formally verified postquantum WireGuard  news.ycombinator.com  20230228 
Project mention: Rosenpass – formally verified postquantum WireGuard  news.ycombinator.com  20230228

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 dependentlytyped 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)  reddit.com/r/rust  20230228 

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)  reddit.com/r/ProgrammingLanguages  20220914
https://github.com/ligurio/practicalfm Look for Coq, Agda, Idris, MS  F*.

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.

awesomecoq
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.  reddit.com/r/math  20230313Coq has an awesome list by the community: https://github.com/coqcommunity/awesomecoq

InfluxDB
Access the most powerful time series database as a service. Ingest, store, & analyze all types of time series data in a fullymanaged, purposebuilt database. Keep data forever with lowcost storage and superior data compression.

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 https://github.com/whonore/Coqtail for that purpose), but neither provides code completion. Nonetheless, thank you so much for your help. Much appreciated.

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?  reddit.com/r/rust  20220608
Coq of OCaml is a good example of how I want it to be for rust


You can check it out here: https://www.principiarewrite.com/

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

Project mention: Let's collect relatively new research programming languages in this thread  reddit.com/r/ProgrammingLanguages  20221115
Jasmin, late 2010s, a language designed to be lowerlevel than C and provide good lowlevel control for cryptographic code. Basically a new take on "C as a highlevel 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.


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





Project mention: Let's collect relatively new research programming languages in this thread  reddit.com/r/ProgrammingLanguages  20221115
https://github.com/kokalang/koka Algebraic effects and reference counting. https://github.com/mitplv/koika hardware description DSL for coq

coqlibraryundecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Project mention: Development Environment with guix shell for Coq Package  reddit.com/r/GUIX  20220821I want to run guix shell to create an environment with the dependencies required to build coqlibraryundecidability.

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


SaaSHub
SaaSHub  Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
coq related posts
 Inspiring OOP examples?
 Rosenpass – formally verified postquantum WireGuard
 Any small/simple proof languages?
 What made you know that you wanted to pursue mathematics?
 Do you do any code in you research or graduate daily basis
 OpenAI might be training its AI technology to replace some software engineers, report says
 Is there a branch of math that studies the processes and skills of problemsolving themselves?

A note from our sponsor  SonarLint
www.sonarlint.org  28 Mar 2023
Index
What are some of the best opensource coq projects? This list will help you:
Project  Stars  

1  coq  4,128 
2  CompCert  1,571 
3  magmide  750 
4  jscoq  471 
5  practicalfm  412 
6  proofs  240 
7  awesomecoq  215 
8  Coqtail  205 
9  coqofocaml  202 
10  CoqEquations  195 
11  principia  190 
12  verdiraft  165 
13  jasmin  146 
14  fourcolor  124 
15  kami  122 
16  ttlite  112 
17  coqserapi  109 
18  corn  106 
19  toychain  103 
20  koika  102 
21  coqlibraryundecidability  93 
22  next700modulesystems  72 
23  vericert  69 