diff --git a/tools/proof-assist/_index.md b/tools/proof-assist/_index.md
new file mode 100644
index 0000000..ac8f673
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/andromeda.md b/tools/proof-assist/andromeda.md
new file mode 100644
index 0000000..9d76e8e
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/arend.md b/tools/proof-assist/arend.md
new file mode 100644
index 0000000..b60f430
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/arvo.md b/tools/proof-assist/arvo.md
new file mode 100644
index 0000000..4867f33
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/aya.md b/tools/proof-assist/aya.md
new file mode 100644
index 0000000..d5c38cb
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/blazeit.md b/tools/proof-assist/blazeit.md
new file mode 100644
index 0000000..c1d6856
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/cur.md b/tools/proof-assist/cur.md
new file mode 100644
index 0000000..b99f445
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/holbert.md b/tools/proof-assist/holbert.md
new file mode 100644
index 0000000..0c5dc97
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/knuckledragger.md b/tools/proof-assist/knuckledragger.md
new file mode 100644
index 0000000..003e72c
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/lambdapi.md b/tools/proof-assist/lambdapi.md
new file mode 100644
index 0000000..42d9fce
--- /dev/null
+++ b/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 
\ No newline at end of file
diff --git a/tools/proof-assist/lisa.md b/tools/proof-assist/lisa.md
new file mode 100644
index 0000000..8ac48e9
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/narya.md b/tools/proof-assist/narya.md
new file mode 100644
index 0000000..78f496e
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/tools/proof-assist/qrhl-tool.md b/tools/proof-assist/qrhl-tool.md
new file mode 100644
index 0000000..5a915cd
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/tools/proof-assist/sasylf.md b/tools/proof-assist/sasylf.md
new file mode 100644
index 0000000..aeeb3e2
--- /dev/null
+++ b/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.
\ No newline at end of file