Theorem Proving
Showing 36 of 72 projects
A Coq framework for implementing, certifying, and executing impure computations with modular verification.
A modular relation algebra library for Rocq (Coq) with reflexive decision tactics for Kleene algebra with tests and related theories.
A Coq plugin enabling proof writing in a natural, handwritten mathematical style to aid students in learning formal proof.
A Coq/SSReflect port of the 'Functional Algorithms Verified' book, formalizing functional data structures and algorithms.
A collection of Python scripts for manipulating Coq developments, including bug minimization and proof automation.
A collection of Python scripts for manipulating Coq developments, including bug minimization and proof automation.
A Coq library providing verified translations between automata, regular expressions, and WS1S logic for regular languages.
A Coq library formalizing graph theory results, including Menger's Theorem, Hall's Marriage Theorem, and Wagner's Theorem.
Coq formalization of program logics (Hoare logic, separation logic, concurrent separation logic) for verifying imperative and concurrent programs.
A Coq library for certifying primality using Pocklington and Elliptic Curve certificates, with efficient modular arithmetic.
A general-purpose Coq library providing an alternative to Coq's standard library with extensionality axioms and enhanced tactics.
Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.
A formal verification of the Feit-Thompson theorem (Odd Order Theorem) using the Coq proof assistant and Mathematical Components library.
A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.
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 Coq formalization of Bourbaki's Elements of Mathematics, covering set theory and number theory using the Mathematical Components library.
A unified Coq library for bit vectors used across multiple MIT research projects.
A Coq library providing lemmas and tactics for reasoning about lists and binary relations.
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq's Hoare Type Theory.
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 Coq library providing arbitrarily large integer and rational numbers (BigN, BigZ, BigQ) for formal verification.
A Coq implementation of Sokoban, the Japanese warehouse keeper puzzle game.
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 generic goal preprocessing tool for proof automation tactics in Coq.
Proof scripts and materials for tutorials on the Mathematical Components library and small-scale reflection in Coq.
A Coq library of formally verified mathematical theorems and tools covering arithmetic, real analysis, and complex analysis.
A web IDE for ACL2 theorem proving with a Kubernetes-based backend, featuring a modern editor and REPL interface.
Ada binding to the Z3 theorem prover for formal verification and constraint solving.
A Coq reimplementation of the Natural Number Game, providing interactive theorem proving exercises for learning mathematical proofs.
Coq lessons and exercises introducing the SSReflect proof language and Mathematical Components library.
A collection of formalized mathematical theories and algorithms extending the Mathematical Components library for Coq.
A certified solver for the 2x2 Rubik's Cube, formally verified in Coq.
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.