SaaSHub helps you find the best software and product alternatives Learn more →
Top 16 Coq coq Projects
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
-
InfluxDB
InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
-
Verdi — a framework for implementing and formally verifying distributed systems (based on Coq).
-
-
verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
-
-
-
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
-
Stream
Stream - Scalable APIs for Chat, Feeds, Moderation, & Video. Stream helps developers build engaging apps that scale to millions with performant and flexible Chat, Feeds, Moderation, and Video APIs and SDKs powered by a global edge network and enterprise-grade infrastructure.
-
-
disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Diesel — a framework for implementation and compositional machine-assisted verification of distributed systems and their clients (based on Coq);
-
-
-
-
-
-
regexp-Brzozowski
Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Coq coq discussion
Coq coq related posts
-
How do modern compilers choose which variables to put in registers?
-
The Illustrated Guide to a PhD
-
CompCert: Formally verified compilers usable for critical embedded software
-
Breaking Bad: How Compilers Break Constant-Time~Implementations
-
Show HN: I made a puzzle game and it gently introduces my fav math mysteries
-
Translation of the Rust's core and alloc crates to Coq for formal verification
-
So you think you know C?
-
A note from our sponsor - SaaSHub
www.saashub.com | 18 Jul 2025
Index
What are some of the best open-source coq projects in Coq? This list will help you:
# | Project | Stars |
---|---|---|
1 | magmide | 825 |
2 | verdi | 606 |
3 | Coq-Equations | 232 |
4 | verdi-raft | 188 |
5 | coq-serapi | 135 |
6 | ConCert | 120 |
7 | coq-library-undecidability | 119 |
8 | toychain | 112 |
9 | disel | 98 |
10 | vericert | 92 |
11 | hs-to-coq | 85 |
12 | aneris | 34 |
13 | coq-simple-io | 33 |
14 | coqoban | 23 |
15 | regexp-Brzozowski | 13 |
16 | doubly-generic | 4 |