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 development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications!
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
《软件基础》中译版 Software Foundations Chinese Translation
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
An axiom-free formalization of category theory in Coq for personal study and practical work
A framework for formally verifying distributed systems implementations in Coq
A gently curated list of companies using verification formal methods in industry
This repo is the new home of Proof General
A port of Coq to Javascript -- Run Coq in your Browser
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Verified Software Toolchain
A verification toolchain for Rust programs
Visual Studio Code extension for Coq
An introductory course to Homotopy Type Theory
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989