Coq coq

Open-source Coq projects categorized as coq

Top 16 Coq coq Projects

  1. magmide

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

  2. 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.

    InfluxDB logo
  3. verdi

    A framework for formally verifying distributed systems implementations in Coq

    Project mention: On Frameworks for Implementing Distributed Protocols | dev.to | 2024-08-29

    Verdi — a framework for implementing and formally verifying distributed systems (based on Coq).

  4. Coq-Equations

    A function definition package for Coq

  5. verdi-raft

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

  6. coq-serapi

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

  7. ConCert

    A framework for smart contract verification in Coq

  8. coq-library-undecidability

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

  9. 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.

    Stream logo
  10. toychain

    A minimalistic blockchain consensus implemented and verified in Coq

  11. disel

    Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

    Project mention: On Frameworks for Implementing Distributed Protocols | dev.to | 2024-08-29

    Diesel — a framework for implementation and compositional machine-assisted verification of distributed systems and their clients (based on Coq);

  12. vericert

    A formally verified high-level synthesis tool based on CompCert and written in Coq.

  13. hs-to-coq

    Convert Haskell source code to Coq source code.

  14. aneris

    Program logic for developing and verifying distributed systems

  15. coq-simple-io

    IO for Gallina

  16. coqoban

    Sokoban (in Coq) [maintainer=@erikmd]

    Project mention: Coqoban: Sokoban (In Coq) | news.ycombinator.com | 2025-04-08
  17. regexp-Brzozowski

    Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

  18. doubly-generic

    Arity-generic datatype-generic, or doubly-generic, programming in Coq.

  19. SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
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).

Coq coq discussion

Log in or Post with

Coq coq related posts

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

Sponsored
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.
www.influxdata.com

Did you know that Coq is
the 94th most popular programming language
based on number of references?