diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index da0928998976c..559f0d7f0b60e 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -9,7 +9,7 @@ on:
     paths:
       - 'library/**'
       - '.github/workflows/kani.yml'
-      - 'scripts/check_kani.sh'
+      - 'scripts/run-kani.sh'
 
 defaults:
   run:
@@ -35,4 +35,11 @@ jobs:
           submodules: true
 
       - name: Run Kani Script
-        run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head
+        run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
+
+      - name: Run Kani Script with --kani-args and -p
+        run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+
+      - name: Run Kani Script without -p
+        working-directory: ${{github.workspace}}/head
+        run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
diff --git a/.gitignore b/.gitignore
index 367d4db4df2f7..9eb2bba2d7422 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,7 +19,9 @@ Session.vim
 ## Build
 /book/
 /build/
+/kani_build/
 /target
+/library/target
 *.rlib
 *.rmeta
 *.mir
diff --git a/library/Cargo.lock b/library/Cargo.lock
index 54ad052c52322..6b72727613c06 100644
--- a/library/Cargo.lock
+++ b/library/Cargo.lock
@@ -72,6 +72,7 @@ version = "0.0.0"
 dependencies = [
  "rand",
  "rand_xorshift",
+ "safety",
 ]
 
 [[package]]
@@ -219,6 +220,39 @@ dependencies = [
  "unwind",
 ]
 
+[[package]]
+name = "proc-macro-error"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
+dependencies = [
+ "proc-macro-error-attr",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro-error-attr"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.86"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
+dependencies = [
+ "unicode-ident",
+]
+
 [[package]]
 name = "proc_macro"
 version = "0.0.0"
@@ -236,6 +270,15 @@ dependencies = [
  "core",
 ]
 
+[[package]]
+name = "quote"
+version = "1.0.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
+dependencies = [
+ "proc-macro2",
+]
+
 [[package]]
 name = "r-efi"
 version = "4.5.0"
@@ -312,6 +355,16 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "safety"
+version = "0.1.0"
+dependencies = [
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.77",
+]
+
 [[package]]
 name = "std"
 version = "0.0.0"
@@ -353,6 +406,27 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "syn"
+version = "1.0.109"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
+dependencies = [
+ "proc-macro2",
+ "unicode-ident",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.77"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "sysroot"
 version = "0.0.0"
@@ -372,6 +446,12 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "unicode-ident"
+version = "1.0.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
+
 [[package]]
 name = "unicode-width"
 version = "0.1.13"
@@ -405,6 +485,12 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "version_check"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
+
 [[package]]
 name = "wasi"
 version = "0.11.0+wasi-snapshot-preview1"
diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh
deleted file mode 100644
index c93499cb7a398..0000000000000
--- a/scripts/check_kani.sh
+++ /dev/null
@@ -1,55 +0,0 @@
-#!/bin/bash
-
-set -e
-
-# Set the working directories
-VERIFY_RUST_STD_DIR="$1"
-KANI_DIR=$(mktemp -d)
-
-RUNNER_TEMP=$(mktemp -d)
-
-# Get the OS name
-os_name=$(uname -s)
-
-# Checkout your local repository
-echo "Checking out local repository..."
-echo
-cd "$VERIFY_RUST_STD_DIR"
-
-# Checkout the Kani repository
-echo "Checking out Kani repository..."
-echo
-git clone --depth 1 -b features/verify-rust-std https://github.com/model-checking/kani.git "$KANI_DIR"
-
-# Check the OS and
-# Setup dependencies for Kani
-echo "Setting up dependencies for Kani..."
-echo
-cd "$KANI_DIR"
-if [ "$os_name" == "Linux" ]; then
-    ./scripts/setup/ubuntu/install_deps.sh
-elif [ "$os_name" == "Darwin" ]; then
-    ./scripts/setup/macos/install_deps.sh
-else
-    echo "Unknown operating system"
-fi
-
-# Build Kani
-echo "Building Kani..."
-echo
-cargo build-dev --release
-# echo "$(pwd)/scripts" >> $PATH
-
-# Run tests
-echo "Running tests..."
-echo
-cd "$VERIFY_RUST_STD_DIR"
-$KANI_DIR/scripts/kani verify-std -Z unstable-options $VERIFY_RUST_STD_DIR/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates
-
-echo "Tests completed."
-echo
-
-# Clean up the Kani directory (optional)
-rm -rf "$KANI_DIR"
-rm -rf "$RUNNER_TEMP"
-# rm -rf "$VERIFY_RUST_STD_DIR"
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
new file mode 100755
index 0000000000000..5c7741e3d98e7
--- /dev/null
+++ b/scripts/run-kani.sh
@@ -0,0 +1,206 @@
+#!/bin/bash
+
+set -e
+
+usage() {
+    echo "Usage: $0 [options] [-p <path>] [--kani-args <command arguments>]"
+    echo "Options:"
+    echo "  -h, --help         Show this help message"
+    echo "  -p, --path <path>  Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory."
+    echo "  --kani-args  <command arguments to kani>  Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument."
+    exit 1
+}
+
+# Initialize variables
+command_args=""
+path=""
+
+# Parse command line arguments
+# TODO: Improve parsing with getopts
+while [[ $# -gt 0 ]]; do
+    case $1 in
+        -h|--help)
+            usage
+            ;;
+        -p|--path)
+            if [[ -n $2 ]]; then
+                path=$2
+                shift 2
+            else
+                echo "Error: Path argument is missing"
+                usage
+            fi
+            ;;
+        --kani-args)
+            shift
+            command_args="$@"
+            break
+            ;;
+        *)
+            break
+            ;;
+    esac
+done
+
+# Set working directory
+if [[ -n "$path" ]]; then
+    if [[ ! -d "$path" ]]; then
+        echo "Error: Specified directory does not exist."
+        usage
+        exit 1
+    fi
+    WORK_DIR=$(realpath "$path")
+else
+    WORK_DIR=$(pwd)
+fi
+
+cd "$WORK_DIR" || exit 1
+
+# Default values
+DEFAULT_TOML_FILE="tool_config/kani-version.toml"
+DEFAULT_REPO_URL="https://github.com/model-checking/kani.git"
+DEFAULT_BRANCH_NAME="features/verify-rust-std"
+
+# Use environment variables if set, otherwise use defaults
+TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
+REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
+BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
+
+os_name=$(uname -s)
+
+# Function to read commit ID from TOML file
+read_commit_from_toml() {
+    local file="$1"
+    if [ ! -f "$file" ]; then
+        echo "Error: TOML file not found: $file" >&2
+        exit 1
+    fi
+    local commit=$(grep '^commit *=' "$file" | sed 's/^commit *= *"\(.*\)"/\1/')
+    if [ -z "$commit" ]; then
+        echo "Error: 'commit' field not found in TOML file" >&2
+        exit 1
+    fi
+    echo "$commit"
+}
+
+clone_repo() {
+    local repo_url="$1"
+    local directory="$2"
+    local branch="$3"
+    local commit="$4"
+    git clone --depth 1 -b "$branch" "$repo_url" "$directory"
+    cd "$directory"
+    git checkout "$commit"
+    cd - > /dev/null
+}
+
+checkout_commit() {
+    local directory="$1"
+    local commit="$2"
+    cd "$directory"
+    git checkout "$commit"
+    cd ..
+}
+
+get_current_commit() {
+    local directory="$1"
+    if [ -d "$directory/.git" ]; then
+        git -C "$directory" rev-parse HEAD
+    else
+        echo ""
+    fi
+}
+
+build_project() {
+    local directory="$1"
+    cd "$directory"
+
+    if [ "$os_name" == "Linux" ]; then
+        ./scripts/setup/ubuntu/install_deps.sh
+    elif [ "$os_name" == "Darwin" ]; then
+        ./scripts/setup/macos/install_deps.sh
+    else
+        echo "Unknown operating system"
+    fi
+
+    cargo build-dev --release
+    cd ..
+}
+
+get_kani_path() {
+    local build_dir="$1"
+    echo "$(realpath "$build_dir/scripts/kani")"
+}
+
+run_kani_command() {
+    local kani_path="$1"
+    shift
+    "$kani_path" "$@"
+}
+
+# Check if binary exists and is up to date
+check_binary_exists() {
+    local build_dir="$1"
+    local expected_commit="$2"
+    local kani_path="$build_dir/scripts/kani"
+
+    if [ -f "$kani_path" ]; then
+        local current_commit=$(get_current_commit "$build_dir")
+        if [ "$current_commit" = "$expected_commit" ]; then
+            return 0
+        fi
+    fi
+    return 1
+}
+
+
+main() {
+    local current_dir=$(pwd)
+    local build_dir="$WORK_DIR/kani_build"
+    local temp_dir_target=$(mktemp -d)
+
+    echo "Using TOML file: $TOML_FILE"
+    echo "Using repository URL: $REPO_URL"
+
+    # Read commit ID from TOML file
+    commit=$(read_commit_from_toml "$TOML_FILE")
+    echo "Kani commit: $commit"
+
+    # Check if binary already exists and is up to date
+    if check_binary_exists "$build_dir" "$commit"; then
+        echo "Kani binary is up to date. Skipping build."
+    else
+        echo "Building Kani from commit: $commit"
+
+        # Remove old build directory if it exists
+        rm -rf "$build_dir"
+        mkdir -p "$build_dir"
+
+        # Clone repository and checkout specific commit
+        clone_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
+
+        # Build project
+        build_project "$build_dir"
+
+        echo "Kani build completed successfully!"
+    fi
+
+    # Get the path to the Kani executable
+    kani_path=$(get_kani_path "$build_dir")
+    echo "Kani executable path: $kani_path"
+
+    echo "Running Kani command..."
+    "$kani_path" --version
+
+    echo "Running Kani verify-std command..."
+    cd $current_dir
+
+    # Run the command with the provided arguments (if any)
+    if [ -n "$command_args" ]; then
+        "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
+    else
+        "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse
+    fi
+}
+
+main
diff --git a/scripts/run_update_with_checks.sh b/scripts/run_update_with_checks.sh
index e7419f34d4901..03c4d1657a911 100755
--- a/scripts/run_update_with_checks.sh
+++ b/scripts/run_update_with_checks.sh
@@ -135,47 +135,47 @@ fi
 
 echo "------------------------------------"
 # Call the first script to update the subtree
-echo "Update subtree in Main"
+echo "Update subtree in main"
 source $BASE_HOME_DIR/scripts/pull_from_upstream.sh "$TEMP_HOME_DIR" $TOOLCHAIN_DATE $COMMIT_HASH
-OUTPUT_SCRIPT1=("$?")
-if [ "${#OUTPUT_SCRIPT1[@]}" -eq 0 ]; then
-    echo "script1.sh failed to run."
+pull_from_upstream=("$?")
+if [ "${#pull_from_upstream[@]}" -eq 0 ]; then
+    echo "pull_from_upstream.sh failed to run."
     exit 1
 else
-    echo "script1.sh completed successfully."
+    echo "Pulled from upstream succesfully."
 fi
 
 # Call the second script
-echo "Running script2.sh..."
+echo "Updating toolchain..."
 source $BASE_HOME_DIR/scripts/update_toolchain_date.sh "$TEMP_HOME_DIR" "$TOOLCHAIN_DATE"
-OUTPUT_SCRIPT2=("$?")
-if [ "${#OUTPUT_SCRIPT2[@]}" -eq 0 ]; then
-    echo "script2.sh failed to run."
+update_toolchain_date=("$?")
+if [ "${#update_toolchain_date[@]}" -eq 0 ]; then
+    echo "update_toolchain_date.sh failed to run."
     exit 1
 else
-    echo "Update toolchain ran successfully."
+    echo "Toolchain updated succesfully."
 fi
 
 # Call the third script
-echo "Running script3.sh..."
+echo "echo "Checking compatiblity with kani..."
 source $BASE_HOME_DIR/scripts/check_rustc.sh "$TEMP_HOME_DIR"
-OUTPUT_SCRIPT3=("$?")
-if [ "${#OUTPUT_SCRIPT3[@]}" -eq 0 ]; then
-    echo "script3.sh failed to run."
+check_rustc=("$?")
+if [ "${#check_rustc[@]}" -eq 0 ]; then
+    echo "check_rustc.sh failed to run."
     exit 1
 else
-    echo "script3.sh completed successfully."
+    echo "Changes compatible with latest rustc."
 fi
 
-# Call the fourth script
-echo "Running script4.sh..."
-source $BASE_HOME_DIR/scripts/check_kani.sh "$TEMP_HOME_DIR"
-OUTPUT_SCRIPT4=("$?")
-if [ "${#OUTPUT_SCRIPT4[@]}" -eq 0 ]; then
-    echo "script4.sh failed to run."
+# Checking compatiblity with kani
+echo "Checking compatiblity with kani..."
+source $BASE_HOME_DIR/run-kani.sh "$TEMP_HOME_DIR"
+run_kani=("$?")
+if [ "${#run_kani[@]}" -eq 0 ]; then
+    echo "run_kani.sh failed to run."
     exit 1
 else
-    echo "script4.sh completed successfully."
+    echo "Changes compatible with kani's features/verify-std branch."
 fi
 
 # TODO: Issue a Pull Request from the sync branch of the temp repo
diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml
new file mode 100644
index 0000000000000..df854dfcfeac2
--- /dev/null
+++ b/tool_config/kani-version.toml
@@ -0,0 +1,5 @@
+# This version should be updated whenever there is a change that makes this version of kani
+# incomaptible with the verify-std repo.
+
+[kani]
+commit = "cda1b30c935c327a8d4ccba0add9f30b9612863f"