170 Open Source Coq Software Projects
Free and open source coq code projects including engines, APIs, generators, and tools.
Coq 3607 ⭐
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 725 ⭐
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Category Theory 610 ⭐
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 108 ⭐
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 127 ⭐
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 73 ⭐
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 39 ⭐
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 39 ⭐
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 29 ⭐
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