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