diff --git a/new-tool.md b/new-tool.md
index c2cc000..77687a9 100644
--- a/new-tool.md
+++ b/new-tool.md
@@ -51,7 +51,7 @@ developers = ${JSON.stringify(developers)}
 licenses = ${JSON.stringify(licenses)}
 inputs = ${JSON.stringify(inputs)}
 interfaces = ${JSON.stringify(interfaces)}
-maintenance = ${JSON.stringify(maintenance)}
+maintenance = [${JSON.stringify(maintenance)}]
 ${maintenance_year}draft = false
 date = ${date}
 +++\n\n`;
diff --git a/tools/sat-smt/rocq.md b/tools/sat-smt/rocq.md
new file mode 100644
index 0000000..bf50139
--- /dev/null
+++ b/tools/sat-smt/rocq.md
@@ -0,0 +1,20 @@
++++
+title = 'Rocq'
+subtitle = 'Interactive Theorem Prover'
+links = [
+	{ title = "Homepage", url = "https://rocq-prover.org/", icon = 'fa-solid fa-home' },
+	{ title = "Source Code", url = "https://github.com/rocq-prover/rocq", icon = 'fa-solid fa-code' },
+]
+applications = ["Theorem Prover"]
+developers = ["Rocq Team"]
+licenses = ["LGPL-2.1"]
+inputs = ["Rocq"]
+interfaces = ["CLI"]
+maintenance = ["Actively Maintained"]
+draft = false
+date = 2025-08-21
++++
+
+A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more. 
+
+The Rocq Prover was formerly known as the Coq Proof Assistant.
\ No newline at end of file