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 framework 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
My personal repository of formally verified mathematics.
LaTTe : a Laboratory for Type Theory experiments (in clojure)
An experimental proof assistant based on a type theory for synthetic ∞-categories.
😎TT
The People's Refinement Logic
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Add a description, image, and links to the proof-assistant topic page so that developers can more easily learn about it.
To associate your repository with the proof-assistant topic, visit your repo's landing page and select "manage topics."