172 Open Source Coq Software Projects
Free and open source coq code projects including engines, APIs, generators, and tools.
Coq 3623 ⭐
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 732 ⭐
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Category Theory 611 ⭐
An axiom-free formalization of category theory in Coq for personal study and practical work
Coqhammer 167 ⭐
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Verdi Raft 153 ⭐
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Coq Ext Lib 109 ⭐
A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
Disel 90 ⭐
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Awesome Coq 129 ⭐
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [[email protected],@palmskog]
Riscvspecformal 69 ⭐
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 69 ⭐
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
Manifesto 60 ⭐
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Coq Library Undecidability 74 ⭐
A library of mechanised undecidability proofs in the Coq proof assistant.
Coq Big O 31 ⭐
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
Pumpkin Patch 38 ⭐
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Ornamental Search 40 ⭐
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Nand2coq 40 ⭐
Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
Oak Hardware 93 ⭐
Formal specification and verification of hardware, especially for security and privacy.
Lecturas_glc 31 ⭐
Readings on computational logic, interactive theorem proving and functional programming.
Chapar 29 ⭐
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [[email protected]]
Aac Tactics 26 ⭐
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [[email protected]]
Lemma Overloading 22 ⭐
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [[email protected]]
Functional Algebra 22 ⭐
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 18 ⭐
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Dot Iris 24 ⭐
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization