The CompCert formally-verified C compiler

Formal Reasoning About Programs

Sail RISC-V model

Verified Software Toolchain

A Learning Environment for Theorem Proving with the Coq proof assistant

Language for high-assurance and high-speed cryptography

A function definition package for Coq

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older versio…

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

Lecture notes for a short course on proving/programming in Coq via SSReflect.

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

A Verified Compiler for Gallina, Written in Gallina

RISC-V Specification in Coq

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

Modeling and Proving in Computational Type Theory

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

A foundational framework for modular cryptographic proofs in Coq

Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).

Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.

Some unstructured notes concerning the Broad tutorial to take place in March 2020

Fork of http://compcert.inria.fr/

RTLCheck

COATCheck

A Coq framework to support structural design and proof of hardware cache-coherence protocols

Released code for the paper: Formalizing SPARCv8 Instruction Set Architecture in Coq (SETTA'17)

Coq support library for Sail instruction set models