diff --git a/.github/TOOL_REQUEST_TEMPLATE.md b/.github/TOOL_REQUEST_TEMPLATE.md
new file mode 100644
index 0000000000000..474b1d089c6ee
--- /dev/null
+++ b/.github/TOOL_REQUEST_TEMPLATE.md
@@ -0,0 +1,31 @@
+_The following form is designed to provide information for your tool that should be included in the effort to verify the Rust standard library. Please note that the tool will need to be **supported** if it is to be included._
+
+## Tool Name
+_Please enter your tool name here._
+
+## Description
+_Please enter a description for your tool and any information you deem relevant._
+
+## Tool Information
+
+* [ ] Does the tool perform Rust verification? 
+* [ ] Does the tool deal with *unsafe* Rust code? 
+* [ ] Does the tool run independently in CI? 
+* [ ] Is the tool open source?
+* [ ] Is the tool under development? 
+* [ ] Will you or your team be able to provide support for the tool?
+
+## Licenses
+_Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s)._
+
+## Steps to Use the Tool
+
+1. [First Step]
+2. [Second Step]
+3. [and so on...]
+
+## Artifacts
+_If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._
+
+## CI & Versioning
+_Please describe how you version the tool and how it will be supported in CI pipelines._
diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml
index 12113728fc722..45a38b3cc2307 100644
--- a/.github/pull_requests.toml
+++ b/.github/pull_requests.toml
@@ -9,5 +9,8 @@ members = [
     "remi-delmas-3000",
     "qinheping",
     "tautschnig",
-    "jaisnan"
+    "jaisnan",
+    "patricklam",
+    "ranjitjhala",
+    "carolynzech"
 ]
diff --git a/README.md b/README.md
index b718f3fc6b1cd..c3c9712cb2669 100644
--- a/README.md
+++ b/README.md
@@ -7,7 +7,8 @@
 This repository is a fork of the official Rust programming
 language repository, created solely to verify the Rust standard
 library. It should not be used as an alternative to the official
-Rust releases.
+Rust releases. The repository is tool agnostic and welcomes the addition of 
+new tools.
 
 The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
 1. Contributing to the core mechanism of verifying the rust standard library
@@ -36,12 +37,14 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
 ## License
 
 ### Kani
-
 Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
 See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details.
 
 ## Rust
-
 Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
 
 See [the Rust repository](https://github.com/rust-lang/rust) for details.
+
+## Introducing a New Tool
+
+Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.
diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md
index 1e7020c52cf53..cb12bfe9fdfbd 100644
--- a/doc/src/challenges/0010-string.md
+++ b/doc/src/challenges/0010-string.md
@@ -1,4 +1,4 @@
-# Challenge X: Memory safety of String
+# Challenge 10: Memory safety of String
 
 - **Status:** Open
 - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61)
diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md
index 3201400eafbc0..fd428366a0674 100644
--- a/doc/src/challenges/0011-floats-ints.md
+++ b/doc/src/challenges/0011-floats-ints.md
@@ -18,7 +18,7 @@ To find the documentation for these methods, navigate first to the [`core::num`
 
 ### Part 1: Unsafe Integer Methods
 
-Prove the absence of undefined behavior in the following methods for each of the listed integers types, given that their safety preconditions are satisfied:
+Prove the absence of undefined behavior in the following methods for each of the listed integer types, given that their safety preconditions are satisfied:
 
 | Method              | Integer Types |
 | :---           |     :---