Lean 4 programming language and theorem prover

An untyped C-like language for verified low-level programming, with a compiler to RISC-V

Implementation of the Google Zero-Knowledge library for Identity Protocols.

Archive for all Coq related OPAM packages organized in various repositories

A set of examples of crypto implementations

The Rocq Prover Website

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

Cryptographic Primitive Code Generation by Fiat

Extracting imperative code from Gallina

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

RISC-V Specification in Coq

Coq library for tactics, basic definitions, sets, maps

Stdlib for the Rocq Prover

Prime numbers for Coq

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

Connecting computational and symbolic crypto models

Foundational Cryptography Framework for machine-checked proofs of cryptography.

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

Verified Software Toolchain

Micromega tactics for Mathematical Components

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

The CompCert formally-verified C compiler

End user documentation for libscopehal

Language for high-assurance and high-speed cryptography

Mathematical Components compliant Analysis Library

Metaprogramming in Coq

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Mirror of BoringSSL