118 Open Source Coq Software Projects
Free and open source coq code projects including engines, APIs, generators, and tools.
Coq 3030 ⭐
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.
Unimath 657 ⭐
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Category Theory 540 ⭐
An axiom-free formalization of category theory in Coq for personal study and practical work
Coqhammer 147 ⭐
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Verdi Raft 140 ⭐
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Coq Ext Lib 95 ⭐
A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
Disel 84 ⭐
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Awesome Coq 76 ⭐
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [[email protected],@palmskog]
Riscvspecformal 65 ⭐
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Next 700 Module Systems 62 ⭐
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
Manifesto 58 ⭐
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Coq Big O 32 ⭐
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
Pumpkin Patch 31 ⭐
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Ornamental Search 33 ⭐
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Nand2coq 28 ⭐
Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
Oak Hardware 33 ⭐
Formal specification and verification of hardware, especially for security and privacy.
Chapar 27 ⭐
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [[email protected]]
Aac Tactics 17 ⭐
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [[email protected],@palmskog]
Lemma Overloading 17 ⭐
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [[email protected]]
Functional Algebra 17 ⭐
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
Fm Notes 15 ⭐
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Dot Iris 17 ⭐
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization