Proof assistants

Software that assists you with doing mathematical proofs on a computer.

List of proof assistants

We sort the list by the theoretical basis on which each proof assistant is based.

Higher-order logic

• Isabelle/HOL
• HOL Light

Martin-Löf type theory

• Intensional type theory
  • Coq
  • Agda
  • Idris
  • Lean
  • Epigram (no longer maintained)
  • Matita (no longer mantained)
• Extensional type theory
  • NuPRL
  • F*
• Homotopy type theory
  • Coq-HoTT (a modded version of Coq to support HoTT proofs)
  • Isabelle/HoTT
• Cubical type theory
  • Cubical Agda
  • Arend
  • redtt
  • cooltt
  • RedPRL

Edinburgh LF

• Twelf
• Abella
• Beluga
• Dedukti

Refinement types

• F*
• Liquid Haskell

First-order logic

• ACL2

Set theory

• Mizar

Hoare/Separation Logic

• Dafny
• Iris

General frameworks

• Isabelle
• Andromeda
• LEGO (dependent types, no longer maintained)