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.
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
《软件基础》中译版 Software Foundations Chinese Translation
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications!
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 port of Coq to Javascript -- Run Coq in your Browser
A gently curated list of companies using verification formal methods in industry
This repo is the new home of Proof General
Verified Software Toolchain
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Visual Studio Code extension for Coq
An introductory course to Homotopy Type Theory
A Coq IDE build on top of Proof General's Coq mode
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