diff --git a/tools/yices.md b/tools/yices.md
new file mode 100644
index 0000000..1e22ec8
--- /dev/null
+++ b/tools/yices.md
@@ -0,0 +1,29 @@
++++
+date = 2024-02-02T04:14:54-08:00
+draft = false
+title = 'Yices 2'
+purposes = ['Verification Tools', 'Analysis Tools']
+techniques = ['Theorem Proving', 'SMT Solving', 'Model Checking']
+domains = ['Software Verification', 'Hardware Verification', 'Embedded Systems']
+languages = ['SMT-LIB', 'Yices language', 'C', 'OCaml', 'Python']
+systems = ['Discrete Systems', 'Concurrent Systems']
+interactions = ['CLI', 'C API', 'OCaml API', 'Python Bindings']
+formalisms = ['first-order logic', 'SMT-LIB', 'quantifier logic', 'bit-vectors', 'arrays', 'uninterpreted functions', 'arithmetic']
+developers = ['SRI International']
+links = [
+    { title = "Homepage", url = "https://yices.csl.sri.com/" },
+    { title = "Source Code", url = "https://github.com/SRI-CSL/yices2" },
+    { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+publications = ['Dutertre2014']
++++
+
+Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.
+
+### Features
+
+- **SMT Solver:** Supports a wide range of theories and quantifiers.
+- **Multi-language APIs:** C, OCaml, Python, and more.
+- **Cross-platform:** Available on Windows, Linux, and macOS.
+- **Active development:** Open source and maintained by SRI International.
+
diff --git a/tools/z3.md b/tools/z3.md
index 5d12275..3d9b2ee 100644
--- a/tools/z3.md
+++ b/tools/z3.md
@@ -1,22 +1,31 @@
 +++
 date = 2024-02-02T04:14:54-08:00
 draft = false
-title = 'Z3 Theorem Prover'
-weight = 10
-purposes = ['test']
-techniques = ['aaa']
-domains = ['tttt']
-languages = ['tttt']
-systems = ['tttt']
-interactions = ['lorem ipsum', 'aranpoxasi', 'aranpsoasi', 'aranpoasai', 'aransdpoasi', 'aranpoaswei', 'aranapoasi', 'aranpoasi', 'aranpoasi', 'aranpoasasdfasfasdfasdfi', 'araafafanpoasi', 'aranpoasi', 'aranpoasi', 'aranpoasadfsi']
-formalisms = ['tttt']
-developers = ['test dev']
+title = 'Z3'
+purposes = ['Verification Tools', 'Analysis Tools']
+techniques = ['Theorem Proving', 'SMT Solving', 'Model Checking']
+domains = ['Software Verification', 'Hardware Verification', 'Embedded Systems']
+languages = ['SMT-LIB', 'Python', 'C++', 'Java', 'C#']
+systems = ['Discrete Systems', 'Concurrent Systems']
+interactions = ['CLI', 'Python API', 'Rust Bindings', 'playground']
+formalisms = ['first-order logic', 'SMT-LIB', 'quantifier logic', 'bit-vectors', 'arrays', 'uninterpreted functions', 'arithmetic']
+developers = ['Microsoft Research']
 links = [
-  { title = "website", url = "https://github.com/Z3Prover/z3" },
-  { title = "code", url = "https://github.com/Z3Prover/z3" },
-  { title = "playground", url = "https://rise4fun.com/z3" }
+    { title = "Homepage", url = "https://github.com/Z3Prover/z3" },
+    { title = "Source Code", url = "https://github.com/Z3Prover/z3" },
+    { title = "Discussions", url = "https://github.com/Z3Prover/z3/discussions" },
+    { title = "Documentation", url = "https://z3prover.github.io/api/html/" },
+    { title = "Playground", url = "https://rise4fun.com/z3" }
 ]
-publications = ['Taylor2023']
+publications = ['deMoura2008']
 +++
 
-desc
\ No newline at end of file
+Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.
+
+### Features
+
+- **SMT Solver:** Supports a wide range of theories and quantifiers.
+- **Multi-language APIs:** Python, C++, Java, .NET, and more.
+- **Cross-platform:** Available on Windows, Linux, and macOS.
+- **Active development:** Open source and maintained by Microsoft Research.
+- **Web Playground:** Try Z3 online at [Rise4Fun](https://rise4fun.com/z3).