Formal Verification
Showing 36 of 178 projects
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 proof of the Four Color Theorem in Coq, including supporting theories for real numbers, plane topology, and combinatorial hypermaps.
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 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 Python implementation of correct-by-construction consensus protocols, including Casper the Friendly Ghost for blockchain.
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 plugin that checks proof witnesses from external SAT/SMT solvers and provides certified decision procedures.
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
A Coq library for deductive synthesis of correct-by-construction abstract data types and parsers.
Lecture materials and Coq source files accompanying YouTube videos on the Software Foundations textbook.
A Coq library containing mechanized reductions to establish undecidability results for problems in logic and computation.
A library of Coq definitions, theorems, and tactics for use in other Coq developments.
A formally verified, portable SPARK 2014 implementation of the NaCl cryptographic library with constant-time algorithms.
Coq code and solutions for exercises from the Coq'Art book, a foundational text on the Coq proof assistant.
A toolset for formal specification and generation of verifiable binary parsers, message generators, and protocol state machines.
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 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.
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.