Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

Formal Reasoning About Programs

Mathematical Components

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Verified Software Toolchain

A Learning Environment for Theorem Proving with the Coq proof assistant

Coq plugin embedding elpi

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

Convert Haskell source code to Coq source code.

A foundational framework for modular cryptographic proofs in Coq

A formalization of the textbook Elements of Set Theory

The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to…

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

My solutions to Software Foundations course in Coq proof assistant.

Probabilistic separation logics for verifying higher-order probabilistic programs.

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx]

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]

A Rocq version of the miniF2F dataset

Certified Equivalence for Protocol Parsers

Verified Forward Erasure Correction in Coq

An OCaml version of the LTac "exploit" tactic, used as a tutorial for writing Coq plugins

A list library using Z index featured with a powerful solver