78,351 visible repositories in the index
1–16 of 16 · Most stars
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.
Plan, apply and roll back changes to a production ontology, with a blast radius report and a proof an auditor can re-check.
Creusot helps you prove your Rust code is correct.
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
Mathematical Components
NASA PVS Library of Formal Developments
formally verified category theory library
A TLA+ interpreter and model checker in TypeScript
Formal proof of the Four Color Theorem [maintainer=@ybertot]
A formalization of geometry in Coq based on Tarski's axiom system
A Lean formalization of the Classification of Finite Simple Groups
A Lean formalization of the Stacks Project
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
The formal proof of the Odd Order Theorem
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]
Formal proof in Coq of Puiseux's Theorem.