Theorem Proving
Showing 36 of 72 projects
An interactive theorem prover providing a formal language to write mathematical definitions, algorithms, and theorems with machine-checked proof development.
An interactive theorem prover providing a formal language to write mathematical definitions, algorithms, and theorems with machine-checked proof development.
A general-purpose functional programming language with dependent types for verified software development.
A Coq library formalizing mathematics using univalent foundations and homotopy type theory.
A language for formally specifying instruction-set architecture (ISA) semantics with tooling for emulators, documentation, and verification.
An axiom-free formalization of category theory in Coq for representation, manipulation, and realization of categorical terms.
An extensive and coherent library of formalized mathematical theories built on the Coq/Rocq proof assistant with SSReflect.
A Coq framework for implementing and formally verifying distributed systems with support for multiple fault models.
A collection of hard-to-discover tips, tricks, and features for the Coq proof assistant.
A JavaScript port of the Coq proof assistant that runs entirely in the browser, enabling interactive theorem proving online.
A research prototype tool for modular formal verification of C, Rust, and Java programs using separation logic.
A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
A lightweight proof assistant for teaching and exploring formal verification, accompanying The Little Prover book.
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources.
A Vim plugin for interactive Rocq (Coq) proof development, providing IDE-like features within the editor.
A formal proof of the Four Color Theorem in Coq, including supporting theories for real numbers, plane topology, and combinatorial hypermaps.
An automated reasoning hammer tool for Rocq that combines learning with external provers to automate proofs in dependent type theory.
A dependable, cross-platform distribution of the Rocq proof assistant with a curated selection of libraries and tools.
A formalization of geometry in Coq based on Tarski's axiom system, containing both foundational and high-school style proofs.
A Coq plugin that embeds the Elpi λProlog interpreter to define new commands and tactics for theorem proving.
A Coq library providing Haskell-like definitions and notations for formalizing Haskell types and functions in Coq.
A Coq plugin that checks proof witnesses from external SAT/SMT solvers and provides certified decision procedures.
A Coq library providing abstract interfaces for mathematical structures using type classes.
Lecture materials and Coq source files accompanying YouTube videos on the Software Foundations textbook.
A library of Coq definitions, theorems, and tactics for use in other Coq developments.
A library for machine-to-machine interaction with the Coq proof assistant, providing serialization of Coq's internal datatypes to JSON or S-expressions.
Coq code and solutions for exercises from the Coq'Art book, a foundational text on the Coq proof assistant.
A textbook on modeling and proving in computational type theory using the Rocq proof assistant.
A formal specification of the RISC-V instruction set architectures (RV32I, RV64I) and extensions (A, M) written in the Coq proof assistant.
A tool that converts Haskell source code into equivalent Coq source code for formal verification.
A Jupyter kernel for the Coq proof assistant, enabling interactive theorem proving in notebooks.
A multi-backend SMT solver frontend for OCaml providing a consistent interface to various solvers.
A Coq library for mechanizing programming language metatheory with locally nameless representation of binders.
A collaborative, community-driven organization for the long-term maintenance and promotion of packages for the Rocq Prover.
A collection of statements and proofs for 100 famous mathematical theorems formalized in the Coq proof assistant.
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.