Top 153 coq open source projects

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

Gallina to Bedrock2 compilation toolkit

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

Partial Commutative Monoids

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

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

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

Template project for program verification in Coq

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Intermediate Memory Model (IMM) and compilation correctness proofs for it

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

Formalization of the polymorphic lambda calculus and its parametricity theorem

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

Archive for all Coq related OPAM packages organized in various repositories

Convert Haskell source code to Coq source code.

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Formalization of the basic actuarial mathematics using Coq

Formalization of Typed Assembly Language (TAL) in Coq

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

A core language for rule-based hardware design 🦑

Coq to OCaml FFI made easy [maintainer=@lthms]

Stable sort algorithms and their stability proofs in Coq

No description or website provided.

Reference sheet for the Coq language.

A minimalistic blockchain consensus implemented and verified in Coq

Coq plugin embedding elpi

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

Proof of concept to generate safe and fast JavaScript

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

A mechanisation of Wasm in Coq

Goose converts a small subset of Go to Coq

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