Close #19

tools/proof-assist/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Proof Assistants"
+layout = "section"
++++
+
+This page lists all of the Proof Assistants on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/proof-assist/andromeda.md

@@ -0,0 +1,18 @@
++++
+title = 'Andromeda'
+subtitle = 'Proof Assistant'
+links = [
+	{ title = "Homepage", url = "https://www.andromeda-prover.org/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/Andromedans/andromeda", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["BSD-3-Clause"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Andromeda 2 is a proof checker for user-definable dependently-typed theories.

tools/proof-assist/arend.md

@@ -0,0 +1,18 @@
++++
+title = 'Arend'
+subtitle = 'Proof Assistant'
+links = [
+	{ title = "Homepage", url = "https://arend-lang.github.io/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/JetBrains/Arend", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["JetBrains"]
+licenses = ["Apache-2.0"]
+inputs = []
+interfaces = ["CLI","Library"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Arend is a theorem prover and a programming language based on Homotopy Type Theory.

tools/proof-assist/arvo.md

@@ -0,0 +1,19 @@
++++
+title = 'Arvo'
+subtitle = 'Proof Assistant'
+links = [	{ title = "Source Code", url = "https://github.com/uwplse/arvo", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["PLSE lab"]
+licenses = []
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2015
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive year="2015">}}
+
+Arvo is a proof assistant from the PLSE lab.

tools/proof-assist/aya.md

@@ -0,0 +1,18 @@
++++
+title = 'Aya Prover'
+subtitle = 'Proof Assistant'
+links = [
+	{ title = "Homepage", url = "https://www.aya-prover.org/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/aya-prover/aya-dev", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["MIT"]
+inputs = []
+interfaces = ["CLI","IDE Integration"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+A proof assistant designed for formalizing math and type-directed programming.

tools/proof-assist/blazeit.md

@@ -0,0 +1,19 @@
++++
+title = 'BlazeIt'
+subtitle = 'Proof Assistant'
+links = [	{ title = "Source Code", url = "https://github.com/pjreddie/blazeit", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["Yolo"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Not Maintained"]
+updated_year = 2015
+draft = false
+date = 2025-08-22
++++
+
+{{<inactive year="2015">}}
+
+A proof assistant.

tools/proof-assist/cur.md

@@ -0,0 +1,16 @@
++++
+title = 'cur'
+subtitle = 'Proof Assistant'
+links = [	{ title = "Source Code", url = "https://github.com/wilbowma/cur", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover","Specification Language"]
+developers = []
+licenses = ["BSD-2-Clause"]
+inputs = ["Cur"]
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+A language with static dependent-types and dynamic types, type annotations and parentheses, theorem proving and meta-programming.

tools/proof-assist/holbert.md

@@ -0,0 +1,16 @@
++++
+title = 'Holbert'
+subtitle = 'Proof Assistant'
+links = [	{ title = "Source Code", url = "https://github.com/liamoc/holbert", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["BSD-3-Clause"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Holbert is an interactive theorem prover, or proof assistant, based on higher order logic and natural deduction. Furthermore, Holbert is graphical.

tools/proof-assist/knuckledragger.md

@@ -0,0 +1,18 @@
++++
+title = 'knuckledragger'
+subtitle = 'Proof Assistant'
+links = [
+	{ title = "Homepage", url = "https://www.philipzucker.com/knuckledragger/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/philzook58/knuckledragger", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["MIT"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Knuckledragger is an attempt at creating a down to earth, highly automated interactive proof assistant in python. The goal is to support applications like software/hardware verification, calculus, equational reasoning, and numerical bounds.

tools/proof-assist/lambdapi.md

@@ -0,0 +1,16 @@
++++
+title = 'Lambdapi'
+subtitle = 'Proof Assistant'
+links = [	{ title = "Source Code", url = "https://github.com/Deducteam/lambdapi", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = []
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+ Proof assistant based on the λΠ-calculus modulo rewriting 

tools/proof-assist/lisa.md

@@ -0,0 +1,16 @@
++++
+title = 'LISA'
+subtitle = 'Proof Assistant'
+links = [	{ title = "Source Code", url = "https://github.com/epfl-lara/lisa", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["Apache-2.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+LISA is a proof assistant based on first-order logic sequent calculus and set theory.

tools/proof-assist/narya.md

@@ -0,0 +1,16 @@
++++
+title = 'Narya'
+subtitle = 'Proof Assistant'
+links = [	{ title = "Source Code", url = "https://github.com/gwaithimirdain/narya", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["GPL-3.0"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Narya: A proof assistant for higher-dimensional type theory

tools/proof-assist/qrhl-tool.md

@@ -0,0 +1,18 @@
++++
+title = 'Qrhl-tool'
+subtitle = 'Proof Assistant'
+links = [
+	{ title = "Homepage", url = "https://dominique-unruh.github.io/qrhl-tool/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/dominique-unruh/qrhl-tool", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = ["MIT"]
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically for quantum and post-quantum security proofs.

tools/proof-assist/sasylf.md

@@ -0,0 +1,18 @@
++++
+title = 'SASyLF'
+subtitle = 'Proof Assistant'
+links = [
+	{ title = "Homepage", url = "https://www.cs.cmu.edu/~aldrich/SASyLF/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/boyland/sasylf", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = []
+licenses = []
+inputs = []
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-22
++++
+
+SASyLF (pronounced "Sassy Elf") is an LF-based proof assistant specialized to checking theorems about programming languages and logics.