Coq24lgpl-3.0

5 months ago

Some scripts to help construct small reproducing examples of bugs, implement [Pr

Python35mit

6 months ago

Visual Studio Code Extension and Language Server Protocol for Coq

OCaml109lgpl-2.1

5 months ago

coqideinteractive-theorem-proving

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

OCaml116other

5 months ago

coqjsonmachine-learning-api

A Coq library for Homotopy Type Theory

Coq1214other

5 days ago

homotopy-type-theorytype-theoryunivalent-foundations

Various useful scripts for dealing with Coq files

Coq8mit

6 months ago

A library for formalizing Haskell types and functions in Coq

Coq161bsd-3-clause

6 months ago

Coq plugin embedding elpi

Coq114lgpl-2.1

5 months ago

coqextension-languagelambda-prolog

RISC-V Specification in Coq

Coq89bsd-3-clause

11 months ago

Library to create Coq record update functions

Coq40mit

5 months ago

Tricks you wish the Coq manual told you

Coq458

9 months ago

coq

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

Coq98mpl-2.0

6 months ago

coq

A mechanisation of Wasm in Coq

Coq83mit

5 months ago

coqwasmwebassembly

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

HTML50other

10 months ago

coqtheorems

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

Coq82lgpl-2.1

5 months ago

coqcoq-cicoq-platform

A function definition package for Coq

Coq205lgpl-2.1

5 months ago

coqdependent-typesprogramming-language

Convert Haskell source code to Coq source code.

Coq71mit

9 months ago

coqhaskell

Coq is a formal proof management system. It provides a formal language to write

OCaml4576lgpl-2.1

last month

coqdependent-typesproof-assistant

A curated list of awesome Coq libraries, plugins, tools, verification projects,

280cc0-1.0

2 months ago

awesomeawesome-listcoq

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liy

Coq121bsd-2-clause

6 months ago

coqcoq-cicoq-platform

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

Coq92mit

9 months ago

coqcoq-artdocker-coq-action

Docker images of the Coq proof assistant (see also: https://github.com/coq-commu

Dockerfile32bsd-3-clause

7 months ago

cicoqdocker-coq

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zim

Nix31mit

5 months ago

coqnix

Multi platform setup for Coq, Coq libraries and tools

Shell162cc0-1.0

5 months ago

Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

Coq38other

5 months ago

coqcoq-nix-toolboxcoq-platform

Formal verification for OCaml

OCaml236mit

3 months ago

compilercoqocaml

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used t

Coq23lgpl-2.1

5 months ago

coqcoq-cicoq-platform

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

Coq65other

5 months ago

coqcoq-cicoq-platform

Documentation on goals of the coq-community organization, the shared contributin

68other

9 months ago

community-drivencoqmanifesto

Coq plugin for parametricity [maintainer=@proux01]

Coq44other

5 months ago

coqcoq-cicoq-platform

A Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynh

OCaml272mit

5 months ago

coqeditorvscode

IO for Gallina

Coq28mit

5 months ago

coqextractionocaml

Coq plugin providing tactics for rewriting universally quantified equations, mod

OCaml29other

6 months ago

coqcoq-cicoq-platform

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (c

Coq52mit

5 months ago

coqcoq-nix-toolboxdiscrete-mathematics

A Coq formalization of information theory and linear error-correcting codes

Coq60lgpl-2.1

5 months ago

convexityerror-correcting-codesinformation-theory

Monadic effects and equational reasonig in Coq

Coq67lgpl-2.1

5 months ago

math-compmathcompmonad-transformers

A framework for smart contract verification in Coq

Coq98mit

6 months ago

blockchaincoqsmart-contracts

Library for Classical Coq

Coq33other

7 months ago

A collection of tools for writing technical documents that mix Coq code and pros

HTML208mit

5 months ago

A Library for Representing Recursive and Impure Programs in Coq

Coq182mit

6 months ago

A Coq library providing tactics to deal with hypothesis

Coq18mit

5 months ago

coqformal-proofshypothesis

Tool for generating Locally Nameless definitions and proofs in Coq, working toge

Haskell29mit

6 months ago

Prime numbers for Coq

Coq34lgpl-2.1

7 months ago

coqelliptic-curvespocklington-certificate

Solving the mini Rubik (2x2) in Coq

Coq3

10 months ago

2x2x2coqformalization

a version of the 2048 game for Coq

Coq22

6 months ago

2048coqgame

A framework for formally verifying distributed systems implementations in Coq

Coq559bsd-2-clause

6 months ago

coqcoq-librarydistributed-systems

Interactive Coq Proofs in Vim

Python240mit

6 months ago

coqproof-assistantvim

Coq development for the course "Mechanized semantics", Collège de France, 2019-2

Coq48lgpl-2.1

10 months ago

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

Coq108gpl-2.0

6 months ago

coqcoq-cicoq-library

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintain

Coq24mit

6 months ago

bourbakicoqdocker-coq-action

A library of abstract interfaces for mathematical structures in Coq [maintainer=

Coq158mit

6 months ago

coqcoq-cicoq-library

Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly

Coq11

9 months ago

coqmathcompmathcomp-ci

Templates for configuration files and scripts useful for maintaining Coq project

Mustache11unlicense

5 months ago

continuous-integrationcoqmustache-templates

A library for verifying graph-manipulating programs. Powered by Coq and VST. Com

Coq12mit

5 months ago

compcertcoqgraph-algorithms

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

Coq160lgpl-3.0

6 months ago

archimedescontinuitycoq

Randomized Property-Based Testing Plugin for Coq

Coq233other

5 months ago

coqtesting

Communication between Coq and SAT/SMT solvers

OCaml145other

5 months ago

A foundational framework for modular cryptographic proofs in Coq

Coq46mit

7 months ago

coq-formalizationcoq-librarycryptography

An enhanced unification algorithm for Coq

OCaml46mit

5 months ago

Coq library on rewriting theory and termination

Coq32other

6 months ago

Relation algebra library for Coq

Coq41lgpl-3.0

6 months ago

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

Coq716bsd-3-clause

5 months ago

cartesiancartesian-closed-categorycategories

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dep

OCaml192other

5 months ago

automationcoqdependent-types

Metaprogramming in Coq

Coq311mit

5 months ago

coqcoq-formalizationmetaprogramming

Hanoi tower in Coq

Coq23mit

6 months ago

This coq library aims to formalize a substantial body of mathematics using the u

Coq876other

5 months ago

coqcoq-libraryfoundations

An implementation of the Raft distributed consensus protocol, verified in Coq us

Coq175bsd-2-clause

6 months ago

consensuscoqdistributed-systems

Hahn: A Coq library

Coq28mit

7 months ago

coq-library

VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Co

Coq20lgpl-3.0

6 months ago

Completeness and Decidability of Modal Logic Calculi [maintainer=@chdoc]

Coq8other

10 months ago

coqctlmathcomp

Docker images of coq-mathcomp [maintainer=@erikmd]

Dockerfile6bsd-3-clause

6 months ago

cicoqdocker-image

Formal proof of the Four Color Theorem [maintainer=@ybertot]

Coq135other

6 months ago

coqcoq-cifour-color-theorem

Graph Theory [maintainers=@chdoc,@damien-pous]

Coq28

6 months ago

coqdocker-coq-actiongraph-theory

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

Emacs Lisp340gpl-3.0

last year

company-modecoqemacs

Sokoban (in Coq) [maintainer=@erikmd]

Coq21lgpl-2.1

last year

coqcoq-librarypuzzle

Libraries demonstrating design patterns for programming and proving with canonic

Coq26other

2 years ago

automationcanonical-structurescoq

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

2other

2 years ago

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@v

Coq23lgpl-2.1

2 years ago

coqmonadpaper-artifacts

A certified Sudoku solver in Coq [maintainers=@siraben,@thery]

Coq20lgpl-2.1

last year

coqnix-actionsudoku

Python bindings for the Coq interactive proof assistant

OCaml48

2 years ago

coqmachine-learningpython

Tool for suggesting lemma names in Coq verification projects

Python15mit

2 years ago

coqdeep-learningmachine-learning

Jupyter kernel for Coq

Python86apache-2.0

2 years ago

coqdependent-typesjupyter

Formal proof in Coq of Puiseux's Theorem.

Coq4other

2 years ago

Verified hash-based AMQ structures in Coq

Coq120gpl-3.0

4 years ago

amqbloom-filtercoq

An HTML documentation generator for Coq source files

OCaml26gpl-2.0

3 years ago

A generic goal preprocessing tool for proof automation tactics in Coq

Prolog12lgpl-3.0

last year

Mutation analysis tool for Coq verification projects

Java25apache-2.0

4 years ago

coqmutation-analysisserapi

A framework for implementing and certifying impure computations in Coq

Coq49mpl-2.0

2 years ago

coqformal-verificationfreer-monads

Coqtail is a library of mathematical theorems and tools proved inside the Coq pr

Coq13other

last year

complex-analysiscoqreal-analysis

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpr

Coq193other

5 years ago

Formalization of Tarjan 72 algorithm in Coq with mathematical components and ssr

Coq9

last year

coqmathcompssreflect

Reimplementation of Natural Number Game in Coq

Coq6apache-2.0

last year

coqgamelean

Companion Coq development for Xavier Leroy's 2021 lectures on program logics

Coq32

3 years ago