166 Open source projects that are alternatives of or similar to Coq

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

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

Jupyter kernel for Coq

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

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

Mtac in Agda

LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.

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

A Coq library providing tactics to deal with hypothesis

Archive for all Coq related OPAM packages organized in various repositories

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

GAPT: General Architecture for Proof Theory

Ltac2 tutorial

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.

Template project for program verification in Coq

Multinomials for the Mathematical Components library.

Formalization of the polymorphic lambda calculus and its parametricity theorem

A gently curated list of companies using verification formal methods in industry

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics

A framework for implementing and certifying impure computations in Coq

Formal verification of OCaml programs

An inference engine for extensional untyped λ-calculus

No description or website provided.

Formalization of Typed Assembly Language (TAL) in Coq

A core language for rule-based hardware design 🦑

Finite sets, finite maps, multisets and generic sets

Public code developed during my MSc study at University of Bologna

Book: Gentle Introduction to Dependent Types with Idris

Gallina to Bedrock2 compilation toolkit

IO for Gallina

Partial Commutative Monoids

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Convert Haskell source code to Coq source code

An SMT Solver for string constraints

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

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

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

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

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

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

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

Convert Haskell source code to Coq source code.

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

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

A proof of Abel-Ruffini theorem.

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

Stable sort algorithms and their stability proofs in Coq

Formalization of the basic actuarial mathematics using Coq

Verified Software Toolchain

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

The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.

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

No description or website provided.

The formal proof of the Odd Order Theorem

Tricks you wish the Coq manual told you

An introductory course to Homotopy Type Theory

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Mutation analysis tool for Coq verification projects