Formal Verification
Showing 36 of 178 projects
A general-purpose Coq library providing an alternative to Coq's standard library with extensionality axioms and enhanced tactics.
A SPARK/Ada implementation of the Keccak family of cryptographic sponge functions, including SHA-3, with formal proof of type safety.
Docker images for Coq proof assistant versions 8.4 to 8.20, based on Debian Slim with opam 2.x.
Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.
A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.
A formal verification of the Feit-Thompson theorem (Odd Order Theorem) using the Coq proof assistant and Mathematical Components library.
A Coq plugin providing tactics for rewriting universally quantified equations modulo associativity and commutativity.
Ada and SPARK firmware for the Crazyflie 2.0 nano quadcopter, targeting the STM32F4 ARM chip.
A flexible Ada library offering generic containers and algorithms with SPARK compatibility and performance control.
A Coq library formalizing Partial Commutative Monoids (PCMs) for separation logic-based program verification.
A library providing a purely functional IO monad for Coq, enabling direct implementation of IO programs with OCaml bindings.
Generates locally nameless definitions and infrastructure lemmas for Coq from Ott language specifications.
A partial implementation of Protocol Buffers in Idris, leveraging dependent types for type-safe serialization without code generation.
An HTML documentation generator for Coq source files with proof script folding capabilities.
A Coq formalization of Bourbaki's Elements of Mathematics, covering set theory and number theory using the Mathematical Components library.
A unified Coq library for bit vectors used across multiple MIT research projects.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
A Coq library providing lemmas and tactics for reasoning about lists and binary relations.
A cryptographic library in SPARK 2014
A Java static analysis tool that translates Java code into LiSA's IR and runs configurable abstract interpretation analyses for bug detection and verification.
A minimalistic, security-focused x86-64 operating system kernel written in Ada/SPARK with formal verification.
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq's Hoare Type Theory.
A static analyzer performing shape analysis on memory structures in programs.
A formal Coq development of the Tower of Hanoi problem with generalized frameworks and proofs.
A Coq library providing enhanced coinductive proof methods based on the 'companion' concept from coinduction theory.
A graphics initialization library for embedded environments, written in SPARK Ada and supporting Intel Core processors.
A Coq library for formal verification of randomized algorithms using a monadic probability distribution interpretation.
A Rocq library providing stable mergesort algorithms with formal correctness proofs using relational parametricity.
A Coq library providing arbitrarily large integer and rational numbers (BigN, BigZ, BigQ) for formal verification.
A Coq implementation of Sokoban, the Japanese warehouse keeper puzzle game.
GitHub Action to set up Ada and SPARK development environments for CI/CD workflows.
A SPARK library for building portable, verifiable, and high-performance trusted components in component-based systems.
A formally verified XML library in SPARK 2014, proven free of runtime errors and with bounded stack usage for secure untrusted data processing.
A Coq library providing tactics and tacticals for hypothesis manipulation during proofs.
A neural network-based tool that suggests lemma names for Coq verification projects by analyzing serialized statements and elaborated terms.
A formal verification of the 2048 game implemented 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.