Proof Assistant
Showing 36 of 106 projects
A Coq framework for formal verification, property-based testing, and extraction of smart contracts.
A textbook on modeling and proving in computational type theory using the Rocq proof assistant.
A Coq library for formally verifying probabilistic properties of hash-based approximate membership query structures like Bloom filters.
A mechanized formalization of WebAssembly 2.0 in Coq (Rocq) with soundness proofs and an extracted interpreter.
A formal specification of the RISC-V instruction set architectures (RV32I, RV64I) and extensions (A, M) written in the Coq proof assistant.
A Coq library for constructive real analysis and algebra, including a model of real numbers and exact real computation.
A Coq plugin providing high-level commands to declare and manage hierarchies of algebraic structures using packed classes.
A Coq plugin that extracts dependency graphs between Coq objects and provides tools for visualization and analysis.
A Jupyter kernel for the Coq proof assistant, enabling interactive theorem proving in notebooks.
A foundational framework for modular cryptographic proofs in the Coq proof assistant, enabling state-separating proofs.
A Coq-based project exploring hydra battles, ordinal numbers, addition chains, and Gödel's incompleteness theorem through formalized mathematics.
A Coq library for mechanizing programming language metatheory with locally nameless representation of binders.
A Rocq library for formal reasoning about discrete probabilities, information theory, and linear error-correcting codes.
A Rocq library providing a formalized hierarchy of monads and their laws for monadic equational reasoning.
A Coq library for effective algebra, providing optimized algorithms and a refinement framework for changing data representations in proofs.
A Coq-based competition for formally proving the largest constructive number within computational constraints.
A collection of statements and proofs for 100 famous mathematical theorems formalized in the Coq proof assistant.
A Coq plugin that replaces Coq's standard unification algorithm with an enhanced one supporting universe polymorphism and overloading.
A framework for developing and verifying domain-specific languages, with a focus on query, rules, and smart contract languages.
Python bindings and libraries for interacting with the Coq interactive proof assistant programmatically.
A typed tactic language plugin for Coq that enables backward reasoning with a monadic interface.
A Coq framework for machine-checked proofs of cryptographic security in the computational model.
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 library extending Mathematical Components with finite sets, finite maps, and multisets on choicetypes.
A Coq plugin enabling proof writing in a natural, handwritten mathematical style to aid students in learning formal proof.
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 that automatically generates record update functions using typeclasses and Ltac2.
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.
An educational environment for writing mathematical proofs in interactive notebooks, now available as a VS Code extension.
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.
Docker images for Coq proof assistant versions 8.4 to 8.20, based on Debian Slim with opam 2.x.
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.