Coq
Showing 36 of 80 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 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.
Synthesizes formally verified, correct-by-construction C, Rust, Go, and other language code for cryptographic field arithmetic primitives.
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 project formalizing the Rocq proof assistant in Rocq itself, providing tools for metaprogramming and developing certified plugins.
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 tool for writing definitions of programming languages and calculi, generating LaTeX and formal proof assistant code from a concise ASCII notation.
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 language and compiler for writing high-assurance, high-speed cryptographic implementations.
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 and absence of failures.
Translates OCaml programs to Coq for formal verification of properties like invariants, absence of failures, and backward compatibility.
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.
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 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 formally verified implementation of the Raft distributed consensus protocol in Coq using the Verdi framework.
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 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.
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.