diff --git a/_index.md b/_index.md
index c440846..0ca0b8d 100644
--- a/_index.md
+++ b/_index.md
@@ -11,11 +11,11 @@ From decades-old classics to cutting-edge tools, this site aims to put as much i
 
 Below are some quick links that may be helpful, plus a random selection of tools (refreshed every time I push updates to this site). 
 
-{{<button href="/applications/smt-solver/">}}
-SMT Solvers
+{{<button href="/tools">}}
+List of Tools
 {{</button>}} 
-{{<button href="/applications/model-checker/">}}
-Model Checkers
+{{<button href="/taxonomies">}}
+Taxonomy Data
 {{</button>}} 
 {{<button href="/contribute">}}
 Contribute
diff --git a/tools/mc/_index.md b/tools/mc/_index.md
new file mode 100644
index 0000000..55e741a
--- /dev/null
+++ b/tools/mc/_index.md
@@ -0,0 +1,10 @@
++++
+title = "Model Checking Tools"
+layout = "section"
++++
+
+This page lists all of the model checking tools 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/mc/sally.md b/tools/mc/sally.md
new file mode 100644
index 0000000..d0b2fbf
--- /dev/null
+++ b/tools/mc/sally.md
@@ -0,0 +1,24 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Sally'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "http://sri-csl.github.io/sally/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/SRI-CSL/sally", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['SRI International']
+licenses = ['GPLv2']
+inputs = ['Sally']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2023">}} -->
+
+
+Sally is a model checker for infinite state systems described as transition systems.
\ No newline at end of file
diff --git a/tools/pmc/stamina.md b/tools/pmc/stamina.md
deleted file mode 100644
index 687636a..0000000
--- a/tools/pmc/stamina.md
+++ /dev/null
@@ -1,22 +0,0 @@
-+++
-date = 2025-06-07
-draft = true
-title = 'STAMINA TODO'
-subtitle = 'Probabilistic Model Checker'
-links = [
-    { title = "Homepage", url = "https://cvc5.github.io/", icon = 'fa-solid fa-home' },
-    { title = "Source Code", url = "https://github.com/dreal/dreal4", icon = 'fa-brands fa-github'  },
-    { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
-]
-applications = ['Probabilistic Model Checker', 'Rare Events']
-developers = ['Utah State University']
-licenses = ['BSD']
-inputs = ['SMTLIB2']
-interfaces = ['CLI', 'Online']
-maintenance = ['Actively Maintained']
-# techniques = ['CDCL']
-publications = ['Barbosa2022']
-+++
-
-<!-- {{<inactive year="2023">}} -->
-cvc5 is an automatic theorem prover for SMT problems.
\ No newline at end of file
diff --git a/tools/pmc/_index.md b/tools/prob/_index.md
similarity index 75%
rename from tools/pmc/_index.md
rename to tools/prob/_index.md
index e9cbb12..d937c1e 100644
--- a/tools/pmc/_index.md
+++ b/tools/prob/_index.md
@@ -1,9 +1,9 @@
 +++
-title = "All PMC Tools"
+title = "Probabilistic Tools"
 layout = "section"
 +++
 
-This page lists all of the SAT & SMT tools on this site in alphabetical order.
+This page lists all of the probabilistic tools 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. 
diff --git a/tools/prob/prism.md b/tools/prob/prism.md
new file mode 100644
index 0000000..c27c001
--- /dev/null
+++ b/tools/prob/prism.md
@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'PRISM'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://prismmodelchecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Oxford University']
+licenses = ['GPLv2']
+inputs = ['PRISM', 'MRMC']
+interfaces = ['CLI', 'Java']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Kwiatkowska2011']
++++
+
+<!-- {{<inactive year="2023">}} -->
+PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.
\ No newline at end of file
diff --git a/tools/prob/stamina.md b/tools/prob/stamina.md
new file mode 100644
index 0000000..e8d68c6
--- /dev/null
+++ b/tools/prob/stamina.md
@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'STAMINA'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://staminachecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://staminachecker.org/source.html", icon = 'fa-brands fa-github'  },
+    { title = "Playground", url = "https://staminachecker.org/run.html", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Utah State University']
+licenses = ['MIT', 'GPLv3']
+inputs = ['PRISM']
+interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Jeppson2023']
++++
+
+<!-- {{<inactive year="2023">}} -->
+ A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either [Storm](../storm) or [PRISM](../prism).
\ No newline at end of file
diff --git a/tools/prob/storm.md b/tools/prob/storm.md
new file mode 100644
index 0000000..a8ba51a
--- /dev/null
+++ b/tools/prob/storm.md
@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Storm'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://www.stormchecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['RWTH Aachen']
+licenses = ['GPLv3']
+inputs = ['PRISM', 'JANI', 'PNML', 'GreatSPN', 'Galileo', 'MRMC']
+interfaces = ['CLI', 'C++', 'Python']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Hensel2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Storm is a tool for the analysis of systems involving random or probabilistic phenomena. 
\ No newline at end of file
diff --git a/tools/sat-smt/_index.md b/tools/sat-smt/_index.md
index 89d3e3b..0d5a6e9 100644
--- a/tools/sat-smt/_index.md
+++ b/tools/sat-smt/_index.md
@@ -1,5 +1,5 @@
 +++
-title = "All SAT & SMT Tools"
+title = "SAT & SMT Tools"
 layout = "section"
 +++
 
diff --git a/tools/sat-smt/lingeling.md b/tools/sat-smt/lingeling.md
index 1f914e3..06240df 100644
--- a/tools/sat-smt/lingeling.md
+++ b/tools/sat-smt/lingeling.md
@@ -2,7 +2,7 @@
 date = 2025-06-07
 draft = false
 title = 'Lingeling'
-subtitle = 'SMT Solver'
+subtitle = 'SAT Solver'
 links = [
     { title = "Homepage", url = "https://fmv.jku.at/lingeling/", icon = 'fa-solid fa-home' },
     { title = "Source Code", url = "https://github.com/arminbiere/lingeling", icon = 'fa-brands fa-github'  },
diff --git a/tools/termination/_index.md b/tools/termination/_index.md
index 85d4237..4f161dd 100644
--- a/tools/termination/_index.md
+++ b/tools/termination/_index.md
@@ -1,5 +1,5 @@
 +++
-title = "All Termination Tools"
+title = "Termination Tools"
 layout = "section"
 +++