Frameworks
9 projects
ConCertA Coq framework for formal verification, property-based testing, and extraction of smart contracts.
CoqEALA Coq library for effective algebra, providing optimized algorithms and a refinement framework for changing data representations in proofs.
FiatA Coq library for deductive synthesis of correct-by-construction abstract data types and parsers.
Hoare Type TheoryA verification system for reasoning about heap-manipulating programs using Separation logic embedded in Coq.
SSProveA foundational framework for modular cryptographic proofs in the Coq proof assistant, enabling state-separating proofs.
VerdiA Coq framework for implementing and formally verifying distributed systems with support for multiple fault models.
User Interfaces
9 projects
CoqtailA Vim plugin for interactive Rocq (Coq) proof development, providing IDE-like features within the editor.
Coq LSPA language server and VS Code extension providing incremental checking, error recovery, and IDE features for the Rocq/Coq proof assistant.
Company-CoqA collection of Emacs extensions for Proof General's Coq mode, providing IDE-like features for interactive theorem proving.
jsCoqA JavaScript port of the Coq proof assistant that runs entirely in the browser, enabling interactive theorem proving online.
Jupyter kernel for CoqA Jupyter kernel for the Coq proof assistant, enabling interactive theorem proving in notebooks.
VsCoqA Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
VsCoq LegacyA Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
Libraries
9 projects
coq-haskellA Coq library providing Haskell-like definitions and notations for formalizing Haskell types and functions in Coq.
ExtLibA library of Coq definitions, theorems, and tactics for use in other Coq developments.
Formalised Undecidable ProblemsA Coq library containing mechanized reductions to establish undecidability results for problems in logic and computation.
Interaction TreesA Coq library for representing and reasoning about recursive, effectful, and non-terminating programs using interaction trees.
MetalibA Coq library for mechanizing programming language metatheory with locally nameless representation of binders.
Package and Build Management
8 projects
Coq PlatformA dependable, cross-platform distribution of the Rocq proof assistant with a curated selection of libraries and tools.
Plugins
11 projects
Coq-ElpiA Coq plugin that embeds the Elpi λProlog interpreter to define new commands and tactics for theorem proving.
CoqHammerAn automated reasoning hammer tool for Rocq that combines learning with external provers to automate proofs in dependent type theory.
EquationsA function definition plugin for Rocq/Coq that provides notation for dependent pattern-matching and well-founded recursion.
Hierarchy BuilderA Coq plugin providing high-level commands to declare and manage hierarchies of algebraic structures using packed classes.
MetaCoqA project formalizing the Rocq proof assistant in Rocq itself, providing tools for metaprogramming and developing certified plugins.
QuickChickA randomized property-based testing plugin for Coq, enabling automated test generation and verification within proof assistants.
SMTCoqA Coq plugin that checks proof witnesses from external SAT/SMT solvers and provides certified decision procedures.