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.
Formal verification for AI: a Lean 4 + Dafny proof checker that catches fake AI proofs (reward hacking), and verified recursive self-improvement (RSI) for coding agents. AI for math, physics and software engineering.
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. https://gitlab.epfl.ch/lara/stainless
Proof assistant based on the λΠ-calculus modulo rewriting
Links to tools by subject
A verifier for automated and interactive proofs about transition systems.
A proof assistant and a dependently-typed language
Composable mathematics tools for agents
A Coq IDE build on top of Proof General's Coq mode
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
To associate your repository with the proof-assistant topic, visit your repo's landing page and select "manage topics."