Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

Tricks you wish the Coq manual told you [maintainer=@tchajed]

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

My personal repository of formally verified mathematics.

Convert Haskell source code to Coq source code

A Library for Representing Recursive and Impure Programs in Coq

A function definition package for Rocq

Formal proof of the Four Color Theorem [maintainer=@ybertot]

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

🐣 A blog engine written and proven in Coq

A library for formalizing Haskell types and functions in Coq

Mostly Automated Synthesis of Correct-by-Construction Programs

Coq formalizations of functional languages.

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

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

A library of mechanised undecidability proofs in the Coq proof assistant.

PeaCoq is a pretty Coq, isn't it?

A formally verified high-level synthesis tool based on CompCert and written in Coq.

Formalization of C++ for verification purposes.

Lecture material for DeepSpec Summer School 2017

The Penn Locally Nameless Metatheory Library

Monadic effects and equational reasoning in Rocq

A formalisation of the Calculus of Constructions

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

A Specification for Dependent Types in Haskell (Core)

Compilation and Verification of Data-Centric Languages

Relation algebra library for Coq

Total Parser Combinators in Coq [maintainer=@womeier]

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…