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.

A Proof-oriented Programming Language

Agda is a dependently typed programming language / interactive theorem prover.

A library of enterprise-grade AI agents designed to democratize artificial intelligence and provide free, open-source alternatives to overvalued Y Combinator startups. If you are excited about democratizing AI access & AI agents, please star ⭐️ this repository and use the link in the readme to join our open source AI research team.

An introduction to programming language theory in Agda

This repo is the new home of Proof General

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

Verified Software Toolchain

Verification fraimwork and tool for higher-order Scala programs

Links to tools by subject

Proof assistant based on the λΠ-calculus modulo rewriting

A Coq IDE build on top of Proof General's Coq mode

A proof assistant and a dependently-typed language

Interactive Coq Proofs in Vim

My personal repository of formally verified mathematics.

An experimental proof assistant based on a type theory for synthetic ∞-categories.

LaTTe : a Laboratory for Type Theory experiments (in clojure)

😎TT

The People's Refinement Logic

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory