Theorem Proving
Showing 35 of 35 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.
An automated reasoning hammer tool for Rocq that combines learning with external provers to automate proofs in dependent type theory.
A formal proof of the Four Color Theorem in Coq, including supporting theories for real numbers, plane topology, and combinatorial hypermaps.
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 library providing abstract interfaces for mathematical structures using type classes.
A Coq plugin that checks proof witnesses from external SAT/SMT solvers and provides certified decision procedures.
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.
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.