Coq

A Coq framework for formal verification, property-based testing, and extraction of smart contracts.

A Coq library for effective algebra, providing optimized algorithms and a refinement framework for changing data representations in proofs.

A Coq framework for machine-checked proofs of cryptographic security in the computational model.

A Coq library for deductive synthesis of correct-by-construction abstract data types and parsers.

A Coq framework for implementing, certifying, and executing impure computations with modular verification.

A verification system for reasoning about heap-manipulating programs using Separation logic embedded in Coq.

A framework for developing and verifying domain-specific languages, with a focus on query, rules, and smart contract languages.

A foundational framework for modular cryptographic proofs in the Coq proof assistant, enabling state-separating proofs.

A Coq framework for implementing and formally verifying distributed systems with support for multiple fault models.

A Vim plugin for interactive Rocq (Coq) proof development, providing IDE-like features within the editor.

A language server and VS Code extension providing incremental checking, error recovery, and IDE features for the Rocq/Coq proof assistant.

A collection of Emacs extensions for Proof General's Coq mode, providing IDE-like features for interactive theorem proving.

An Emacs minor mode for selecting and switching between OCaml opam switches via menu or command.

A JavaScript port of the Coq proof assistant that runs entirely in the browser, enabling interactive theorem proving online.

A Jupyter kernel for the Coq proof assistant, enabling interactive theorem proving in notebooks.

A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.

A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.

An educational environment for writing mathematical proofs in interactive notebooks, now available as a VS Code extension.

A partial Tree-sitter grammar for Rocq Prover syntax highlighting in text editors like Helix.

A Coq library for formal verification of randomized algorithms using a monadic probability distribution interpretation.

Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.

A Coq library providing arbitrarily large integer and rational numbers (BigN, BigZ, BigQ) for formal verification.

A unified Coq library for bit vectors used across multiple MIT research projects.

A Coq library for formal verification of graph-manipulating C programs, compatible with CompCert and VST.

A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.

A Coq library providing Haskell-like definitions and notations for formalizing Haskell types and functions in Coq.

A modular Coq library providing constructive, axiom-free proofs of Kruskal's Tree Theorem and related results using almost full relations.

A Coq library that automatically generates record update functions using typeclasses and Ltac2.

A library of Coq definitions, theorems, and tactics for use in other Coq developments.

A Coq library formalizing Partial Commutative Monoids (PCMs) for separation logic-based program verification.

A Coq library containing mechanized reductions to establish undecidability results for problems in logic and computation.

A Coq library providing lemmas and tactics for reasoning about lists and binary relations.

A Coq library for representing and reasoning about recursive, effectful, and non-terminating programs using interaction trees.

A Coq library providing tactics and tacticals for hypothesis manipulation during proofs.

A collection of formalized mathematical theories and algorithms extending the Mathematical Components library for Coq.

Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.

A Coq library for mechanizing programming language metatheory with locally nameless representation of binders.

A Coq library providing verified translations between automata, regular expressions, and WS1S logic for regular languages.

A modular relation algebra library for Rocq (Coq) with reflexive decision tactics for Kleene algebra with tests and related theories.

A library providing a purely functional IO monad for Coq, enabling direct implementation of IO programs with OCaml bindings.

A general-purpose Coq library providing an alternative to Coq's standard library with extensionality axioms and enhanced tactics.

Nix helper scripts to automate local builds and CI for Coq projects, integrating with GitHub Actions and Cachix.

A dependable, cross-platform distribution of the Rocq proof assistant with a curated selection of libraries and tools.

Templates for generating configuration files and boilerplate for Coq projects, including CI setup and documentation.

Docker images for Coq proof assistant versions 8.4 to 8.20, based on Debian Slim with opam 2.x.

Docker images providing stable versions of the Mathematical Components library for the Coq proof assistant.

A Coq plugin providing tactics for rewriting universally quantified equations modulo associativity and commutativity.

A Coq library providing enhanced coinductive proof methods based on the 'companion' concept from coinduction theory.

A Coq plugin that embeds the Elpi λProlog interpreter to define new commands and tactics for theorem proving.

An automated reasoning hammer tool for Rocq that combines learning with external provers to automate proofs in dependent type theory.

A function definition plugin for Rocq/Coq that provides notation for dependent pattern-matching and well-founded recursion.

A Coq plugin providing high-level commands to declare and manage hierarchies of algebraic structures using packed classes.

A project formalizing the Rocq proof assistant in Rocq itself, providing tools for metaprogramming and developing certified plugins.

A typed tactic language plugin for Coq that enables backward reasoning with a monadic interface.

A deprecated Coq plugin for generating parametricity statements and proofs from Coq definitions.

A randomized property-based testing plugin for Coq, enabling automated test generation and verification within proof assistants.

A Coq plugin that checks proof witnesses from external SAT/SMT solvers and provides certified decision procedures.

A Coq plugin that replaces Coq's standard unification algorithm with an enhanced one supporting universe polymorphism and overloading.

A Coq plugin enabling proof writing in a natural, handwritten mathematical style to aid students in learning formal proof.