diff --git a/arewesafetycriticalyet.org/src/components/ToolsList/available-tools.json b/arewesafetycriticalyet.org/src/components/ToolsList/available-tools.json
index 384a8732..5373d059 100644
--- a/arewesafetycriticalyet.org/src/components/ToolsList/available-tools.json
+++ b/arewesafetycriticalyet.org/src/components/ToolsList/available-tools.json
@@ -250,6 +250,13 @@
       "description": "VeriFast is a tool for modular formal verification of the absence of undefined behavior in Rust1 programs that use unsafe blocks and the soundness of Rust modules that use unsafe blocks.",
       "license": "MIT"
     },
+    {
+      "name": "Verus",
+      "type": "formal-verification",
+      "url": "https://github.com/verus-lang/verus",
+      "description": "Verified Rust for low-level systems code.",
+      "license": "MIT"
+    },
     {
       "name": "mutest-rs",
       "type": "testing",