Proof Assistant
Showing 34 of 106 projects
Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.
A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.
A formal verification of the Feit-Thompson theorem (Odd Order Theorem) using the Coq proof assistant and Mathematical Components library.
A Coq plugin providing tactics for rewriting universally quantified equations modulo associativity and commutativity.
A Coq library formalizing Partial Commutative Monoids (PCMs) for separation logic-based program verification.
A library providing a purely functional IO monad for Coq, enabling direct implementation of IO programs with OCaml bindings.
Generates locally nameless definitions and infrastructure lemmas for Coq from Ott language specifications.
An HTML documentation generator for Coq source files with proof script folding capabilities.
A Coq formalization of Bourbaki's Elements of Mathematics, covering set theory and number theory using the Mathematical Components library.
Mutation analysis tool for Coq verification projects to detect incomplete specifications.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
A Coq library providing lemmas and tactics for reasoning about lists and binary relations.
A Coq library for formal verification of randomized algorithms using a monadic probability distribution interpretation.
A Coq library providing enhanced coinductive proof methods based on the 'companion' concept from coinduction theory.
A formal Coq development of the Tower of Hanoi problem with generalized frameworks and proofs.
A Rocq library providing stable mergesort algorithms with formal correctness proofs using relational parametricity.
A Coq library providing arbitrarily large integer and rational numbers (BigN, BigZ, BigQ) for formal verification.
A Coq library providing tactics and tacticals for hypothesis manipulation during proofs.
A neural network-based tool that suggests lemma names for Coq verification projects by analyzing serialized statements and elaborated terms.
A formal verification of the 2048 game implemented in the Coq proof assistant.
A Coq library for formal verification of graph-manipulating C programs, compatible with CompCert and VST.
A certified Sudoku solver implemented in Coq using a formalized Davis-Putnam procedure.
Generates Coq boilerplate code for handling binders, renaming, and substitutions in formal language metatheory.
Coq formalization and correctness proofs of Tarjan's and Kosaraju's algorithms for finding strongly connected components in graphs.
A generic goal preprocessing tool for proof automation tactics in Coq.
A Coq library of formally verified mathematical theorems and tools covering arithmetic, real analysis, and complex analysis.
Machine-checked constructive proofs of soundness, completeness, and decidability for modal logics K, K*, CTL, and PDL.
A collection of utility scripts for working with Coq proof assistant files, including parsing, analysis, and automation tools.
An introductory course on formal verification of floating-point numbers and real numbers using the Coq proof assistant and Flocq library.
A Coq reimplementation of the Natural Number Game, providing interactive theorem proving exercises for learning mathematical proofs.
Docker images providing stable versions of the Mathematical Components library for the Coq proof assistant.
A collection of formalized mathematical theories and algorithms extending the Mathematical Components library for Coq.
An HTML documentation generator for Rocq source files with proof folding, cross-referencing, and Markdown support.
A modular Coq library providing constructive, axiom-free proofs of Kruskal's Tree Theorem and related results using almost full relations.
Related Tags
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.