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. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
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.
Visual Studio Code extension for Coq
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
A verification toolchain for Rust programs
Visual Studio Code Extension and Language Server Protocol for Coq
Archive for all Coq related OPAM packages organized in various repositories
A Seamless, Interactive Tactic Learner and Prover for Coq
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Python bindings for the Coq interactive proof assistant
Automatically generates Coq FFI bindings to OCaml libraries [maintainer=@lthms]
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
A proof tree viewer that works with Coq through Proof General
Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]
Library of useful utility functions for Coq plugins
A project which aim to help engineers to make proves easily
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
Latest release 2 months ago