170 Open Source Coq Software Projects

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.

The CompCert formally-verified C compiler

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

An axiom-free formalization of category theory in Coq for personal study and practical work

Cosette is an automated SQL solver.

《软件基础》中译版 Software Foundations Chinese Translation

A framework for formally verifying distributed systems implementations in Coq

A port of Coq to Javascript -- Run Coq in your Browser

This repo is the new home of Proof General

Mathematical Components

A Coq IDE build on top of Proof General's Coq mode

Tricks you wish the Coq manual told you

A gently curated list of companies using verification formal methods in industry

An introductory course to Homotopy Type Theory

Metaprogramming in Coq

Randomized Property-Based Testing Plugin for Coq

A function definition package for Coq

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

A selection of formal proofs in Coq.

formalization of the Dependent Object Types (DOT) calculus

A formalization of geometry in Coq based on Tarski's axiom system

A Visual Studio Code extension for Coq [[email protected],@fakusb]

Coq formalizations of functional languages.

Import OCaml programs to Coq 🐓 🐫

Verified hash-based AMQ structures in Coq

Lecture notes for a short course on proving/programming in Coq via SSReflect.

A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]

Coq Repository at Nijmegen [[email protected],@VincentSe]

A curated set of links to formal methods involving provable code.

A formalization of category theory in the Coq proof assistant.

A minimalistic blockchain consensus implemented and verified in Coq

Coq Support for Visual Studio Code

A SuperCompiler for Martin-Löf's Type Theory

Interactive Coq Proofs in Vim

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Formal proof of the Four Color Theorem

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

Correctness proofs of Ethereum token contracts

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [[email protected],@palmskog]

Mathematical Components compliant Analysis Library

A Coq-based synthesis of Scala programs which are correct-by-construction

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.

PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

A Learning Environment for Theorem Proving

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.

Archive for all Coq related OPAM packages organized in various repositories

LVC verified compiler

Jupyter kernel for Coq

Coq plugin embedding elpi

Verifying concurrent crash-safe systems

A library of mechanised undecidability proofs in the Coq proof assistant.

Generates natural language versions of Coq proofs

Coq formalizations and proofs of (data) structures and algorithms.

Total Parser Combinators in Coq

Finite sets, finite maps, multisets and generic sets

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

A core language for rule-based hardware design 🦑

General topology in Coq [[email protected],@Columbus240,@stop-cran]

Coq plugin for parametricity [[email protected]]

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).

Formal specification and verification of hardware, especially for security and privacy.

A formally verified high-level synthesis tool based on CompCert and written in Coq.

Readings on computational logic, interactive theorem proving and functional programming.

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [[email protected]]

Mtac in Agda

Coq code and exercises from the Coq'Art book [[email protected],@Casteran]

Goose converts a small subset of Go to Coq

Coq Enhancement Proposals

Hoare Type Theory

Docker images of the Coq proof assistant [[email protected]]

Kami based processor implementations and specifications

Ltac2 tutorial

Formally verified Coq serialization library with support for extraction to OCaml

State-Transition Systems for Smart Contracts

Formalization of the polymorphic lambda calculus and its parametricity theorem

IO for Gallina

Statements of famous theorems proven in Coq [[email protected]]

Collection of scripts to improve the output of coqdoc [[email protected],@palmskog]

Coq utility and tactic library.

Formalization of C++ for verification purposes.

a version of the 2048 game for Coq

Proof of concept to generate safe and fast JavaScript

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [[email protected]]

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [[email protected]]

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.

Coq library for working with de Bruijn indices [[email protected]]

Coq library and tactic for deciding Kleene algebras [[email protected]]

Regular Language Representations in Coq [[email protected],@palmskog]

Partial Commutative Monoids

Mutation analysis tool for Coq verification projects

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization

VERified asSembler for cryptographic primitives

A proof tree viewer that works with Coq through Proof General

Reference sheet for the Coq language.

My attempt to better understand both Coq and Category Theory by formalizing the latter in the former.