The CompCert formally-verified C compiler

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

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

Cryptographic Primitive Code Generation by Fiat

Formal Reasoning About Programs

Mathematical Components

A framework for formally verifying distributed systems implementations in Coq

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

Verified Software Toolchain

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

A work-in-progress language and compiler for verified low-level programming

Language for high-assurance and high-speed cryptography

Convert Haskell source code to Coq source code

Randomized Property-Based Testing Plugin for Coq

FSCQ is a certified file system written and proven in Coq

Please see https://github.com/hacspec/hax

A function definition package for Coq

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

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

A formalization of geometry in Coq based on Tarski's axiom system

🐣 A blog engine written and proven in Coq

A library for formalizing Haskell types and functions in Coq

Coq plugin embedding elpi

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

Programming Language for Smart Legal Contracts

Mostly Automated Synthesis of Correct-by-Construction Programs

A Verified Compiler for Gallina, Written in Gallina

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

A framework for smart contract verification in Coq

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