Open Source Libs
Find Open Source Packages
Open Source Libraries
👉
Coq
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.
Compcert
1341 ⭐
The CompCert formally-verified C compiler
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
Cosette
566 ⭐
Cosette is an automated SQL solver.
Sf Zh
687 ⭐
《软件基础》中译版 Software Foundations Chinese Translation
Verdi
512 ⭐
A framework for formally verifying distributed systems implementations in Coq
Jscoq
418 ⭐
A port of Coq to Javascript -- Run Coq in your Browser
Proofgeneral Pg
405 ⭐
This repo is the new home of Proof General
Math Comp
409 ⭐
Mathematical Components
Company Coq
310 ⭐
A Coq IDE build on top of Proof General's Coq mode
Coq Tricks
341 ⭐
Tricks you wish the Coq manual told you
Practical Fm
339 ⭐
A gently curated list of companies using verification formal methods in industry
Hott Intro
319 ⭐
An introductory course to Homotopy Type Theory
Metacoq
227 ⭐
Metaprogramming in Coq
Quickchick
198 ⭐
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
142 ⭐
A selection of formal proofs in Coq.
Namin Dot
140 ⭐
formalization of the Dependent Object Types (DOT) calculus
Geocoq
137 ⭐
A formalization of geometry in Coq based on Tarski's axiom system
Vscoq
166 ⭐
A Visual Studio Code extension for Coq [
[email protected]
,@fakusb]
Discus Lang Iron
126 ⭐
Coq formalizations of functional languages.
Coq Of Ocaml
157 ⭐
Import OCaml programs to Coq 🐓 🐫
Ceramist
114 ⭐
Verified hash-based AMQ structures in Coq
Pnp
121 ⭐
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Coq Ext Lib
108 ⭐
A library of Coq definitions, theorems, and tactics. [
[email protected]
,@liyishuai]
Corn
101 ⭐
Coq Repository at Nijmegen [
[email protected]
,@VincentSe]
Awesome Provable
138 ⭐
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
146 ⭐
Interactive Coq Proofs in Vim
Disel
90 ⭐
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Fourcolor
100 ⭐
Formal proof of the Four Color Theorem
Coq SerAPI
99 ⭐
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Tokenlibs With Proofs
87 ⭐
Correctness proofs of Ethereum token contracts
Awesome Coq
127 ⭐
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [
[email protected]
,@palmskog]
Analysis
114 ⭐
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
88 ⭐
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
72 ⭐
Coq plugin embedding elpi
Perennial
73 ⭐
Verifying concurrent crash-safe systems
Coq Library Undecidability
73 ⭐
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
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.
Vericert
51 ⭐
A formally verified high-level synthesis tool based on CompCert and written in Coq.
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]
]
Mtacar
29 ⭐
Mtac in Agda
Coq Art
53 ⭐
Coq code and exercises from the Coq'Art book [
[email protected]
,@Casteran]
Tchajed Goose
55 ⭐
Goose converts a small subset of Go to Coq
Ceps
30 ⭐
Coq Enhancement Proposals
Htt
33 ⭐
Hoare Type Theory
Docker Coq
26 ⭐
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
31 ⭐
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
20 ⭐
Coq library and tactic for deciding Kleene algebras [
[email protected]
]
Reglang
25 ⭐
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.