Open Source Libs
Find Open Source Packages
Open Source Libraries
👉
Mathematics
👉
Coq
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.
Compcert
928 ⭐
The CompCert formally-verified C compiler
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
Cosette
521 ⭐
Cosette is an automated SQL solver.
Sf Zh
518 ⭐
《软件基础》中译版 Software Foundations Chinese Translation
Verdi
489 ⭐
A framework for formally verifying distributed systems implementations in Coq
Jscoq
367 ⭐
A port of Coq to Javascript -- Run Coq in your Browser
Proofgeneral Pg
346 ⭐
This repo is the new home of Proof General
Math Comp
320 ⭐
Mathematical Components
Company Coq
283 ⭐
IDE extensions for Proof General's Coq mode
Coq Tricks
275 ⭐
Tricks you wish the Coq manual told you
Practical Fm
236 ⭐
A gently curated list of companies using verification formal methods in industry
Hott Intro
218 ⭐
An introductory course to Homotopy Type Theory
Metacoq
180 ⭐
Metaprogramming in Coq
Quickchick
173 ⭐
Randomized Property-Based Testing Plugin for Coq
Coq Equations
150 ⭐
A function definition package for Coq
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
Proofs
136 ⭐
A selection of formal proofs in Coq.
Namin Dot
132 ⭐
formalization of the Dependent Object Types (DOT) calculus
Geocoq
120 ⭐
A formalization of geometry in Coq based on Tarski's axiom system
Vscoq
120 ⭐
A Visual Studio Code extension for Coq [
[email protected]
]
Discus Lang Iron
113 ⭐
Coq formalizations of functional languages.
Coq Of Ocaml
105 ⭐
Import OCaml programs to Coq 🐓 🐫
Ceramist
105 ⭐
Verified hash-based AMQ structures in Coq
Pnp
101 ⭐
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Coq Ext Lib
95 ⭐
A library of Coq definitions, theorems, and tactics. [
[email protected]
,@liyishuai]
Corn
94 ⭐
Coq Repository at Nijmegen [
[email protected]
,@VincentSe]
Awesome Provable
97 ⭐
A curated set of links to formal methods involving provable code.
Amintimany Categories
87 ⭐
A formalization of category theory in the Coq proof assistant.
Toychain
89 ⭐
A minimalistic blockchain consensus implemented and verified in Coq
Siegebell Vscoq
86 ⭐
Coq Support for Visual Studio Code
Ttlite
87 ⭐
A SuperCompiler for Martin-Löf's Type Theory
Coqtail
93 ⭐
Interactive Coq Proofs in Vim
Disel
84 ⭐
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Fourcolor
79 ⭐
Formal proof of the Four Color Theorem
Coq SerAPI
78 ⭐
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Tokenlibs With Proofs
74 ⭐
Correctness proofs of Ethereum token contracts
Awesome Coq
76 ⭐
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [
[email protected]
,@palmskog]
Analysis
72 ⭐
Mathematical Components compliant Analysis Library
Scallina
61 ⭐
A Coq-based synthesis of Scala programs which are correct-by-construction
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.
Gamepad
61 ⭐
A Learning Environment for Theorem Proving
Manifesto
58 ⭐
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Opam Coq Archive
54 ⭐
Archive for all Coq related OPAM packages organized in various repositories
Lvc
51 ⭐
LVC verified compiler
Coq_jupyter
43 ⭐
Jupyter kernel for Coq
Coq Elpi
42 ⭐
Coq plugin embedding elpi
Perennial
48 ⭐
Verifying concurrent crash-safe systems
Coq Library Undecidability
39 ⭐
A library of formalised undecidable problems in Coq
Coqatoo
38 ⭐
Generates natural language versions of Coq proofs
Foreverbell Verified
38 ⭐
Coq formalizations and proofs of (data) structures and algorithms.
Parseque
36 ⭐
Total Parser Combinators in Coq
Coq Ecosystem
35 ⭐
Finmap
32 ⭐
Finite sets, finite maps, multisets and generic sets
Coq Big O
32 ⭐
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
Koika
37 ⭐
A core language for rule-based hardware design 🦑
Coq Community Topology
32 ⭐
General topology in Coq [
[email protected]
]
Paramcoq
31 ⭐
Coq plugin for parametricity [
[email protected]
]
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.
Vericert
30 ⭐
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Lecturas_glc
27 ⭐
Lecturas del Grupo de Lógica Computacional
Chapar
27 ⭐
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [
[email protected]
]
Mtacar
26 ⭐
Mtac in Agda
Coq Art
29 ⭐
Coq code and exercises from the Coq'Art book [
[email protected]
,@Casteran]
Tchajed Goose
33 ⭐
Goose converts a small subset of Go to Coq
Ceps
22 ⭐
Coq Enhancement Proposals
Htt
23 ⭐
Hoare Type Theory
Docker Coq
20 ⭐
Docker images of the Coq proof assistant [
[email protected]
]
Prockami
20 ⭐
Kami based processor implementations and specifications
Ltac2 Tutorial
21 ⭐
Ltac2 tutorial
Cheerios
19 ⭐
Formally verified Coq serialization library with support for extraction to OCaml
Scilla Coq
18 ⭐
State-Transition Systems for Smart Contracts
System F
19 ⭐
Formalization of the polymorphic lambda calculus and its parametricity theorem
Coq Simple Io
18 ⭐
IO for Gallina
Coq100
21 ⭐
Statements of famous theorems proven in Coq [
[email protected]
]
Coqdoc.js
18 ⭐
Collection of scripts to improve the output of coqdoc [
[email protected]
,@palmskog]
Structtact
18 ⭐
Coq utility and tactic library.
Cpp2v
22 ⭐
Formalization of C++ for verification purposes.
T2048
19 ⭐
a version of the 2048 game for Coq
Coq To Ocaml To JS
19 ⭐
Proof of concept to generate safe and fast JavaScript
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.
Dblib
19 ⭐
Coq library for working with de Bruijn indices [
[email protected]
]
Atbr
16 ⭐
Coq library and tactic for deciding Kleene algebras [
[email protected]
]
Reglang
16 ⭐
Regular Language Representations in Coq [
[email protected]
,@palmskog]
Fcsl Pcm
15 ⭐
Partial Commutative Monoids
Mcoq
16 ⭐
Mutation analysis tool for Coq verification projects
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
Verse Coq
12 ⭐
VERified asSembler for cryptographic primitives
Traf
13 ⭐
A proof tree viewer that works with Coq through Proof General
Coqcheatsheet
12 ⭐
Reference sheet for the Coq language.
Ct
12 ⭐
My attempt to better understand both Coq and Category Theory by formalizing the latter in the former.