Proof Assistant
Showing 36 of 52 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 tool for statically verifying the correctness of Rust code using formal specifications and automated solvers.
A Coq library for formalizing Homotopy Type Theory, interpreting type theory into homotopy theory.
A Coq library formalizing mathematics using univalent foundations and homotopy type theory.
An axiom-free formalization of category theory in Coq for representation, manipulation, and realization of categorical terms.
An automated solver for proving the equivalence of SQL queries using formal verification.
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 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 collection of Emacs extensions for Proof General's Coq mode, providing IDE-like features for interactive theorem proving.
A Vim plugin for interactive Rocq (Coq) proof development, providing IDE-like features within the editor.
A randomized property-based testing plugin for Coq, enabling automated test generation and verification within proof assistants.
Translates OCaml programs to Coq for formal verification of properties like invariants, absence of failures, and backward compatibility.
Translates OCaml programs to Coq for formal verification of properties like invariants and absence of failures.
A formally verified category theory library implemented in Idris, providing correctness guarantees through proofs.
A Coq library for representing and reasoning about recursive, effectful, and non-terminating programs using interaction trees.
A formal real analysis library for the Coq/Rocq proof assistant, built on the Mathematical Components library.
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 function definition plugin for Rocq/Coq that provides notation for dependent pattern-matching and well-founded recursion.
A formalization of geometry in Coq based on Tarski's axiom system, containing both foundational and high-school style proofs.
A language server and VS Code extension providing incremental checking, error recovery, and IDE features for the Rocq/Coq proof assistant.
A Coq plugin that embeds the Elpi λProlog interpreter to define new commands and tactics for theorem proving.
A verified compiler for Gallina (Rocq Prover's specification language) that targets WebAssembly and Clight.
A Coq library providing abstract interfaces for mathematical structures using type classes.
A Coq library for deductive synthesis of correct-by-construction abstract data types and parsers.
A library of Coq definitions, theorems, and tactics for use in other Coq developments.
A Coq library containing mechanized reductions to establish undecidability results for problems in logic and computation.
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.
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.