Coq

#编程语言#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 f...

The CompCert formally-verified C compiler

This rocq 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

Cosette is an automated SQL solver.

Mathematical Components

A framework for formally verifying distributed systems implementations in Coq

A gently curated list of companies using verification formal methods in industry

A port of Coq to Javascript -- Run Coq in your Browser

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

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

#Awesome#A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]