diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml
new file mode 100644
index 0000000000000..84945e236a4ed
--- /dev/null
+++ b/.github/workflows/kani-metrics.yml
@@ -0,0 +1,42 @@
+name: Kani Metrics Update
+
+on:
+  schedule:
+    - cron: '0 0 * * 0'  # Run at 00:00 UTC every Sunday
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  update-kani-metrics:
+    runs-on: ubuntu-latest
+    
+    steps:
+    - name: Checkout Repository
+      uses: actions/checkout@v4
+      with:
+        submodules: true
+    
+    # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
+    - name: Set up Python
+      uses: actions/setup-python@v4
+      with:
+        python-version: '3.x'
+
+    - name: Compute Kani Metrics
+      run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
+
+    - name: Create Pull Request
+      uses: peter-evans/create-pull-request@v7
+      with:
+        commit-message: Update Kani metrics
+        title: 'Update Kani Metrics'
+        body: |
+          This is an automated PR to update Kani metrics.
+          
+          The metrics have been updated by running `./scripts/run-kani.sh --run metrics`.
+        branch: update-kani-metrics
+        delete-branch: true
+        base: main
diff --git a/.gitignore b/.gitignore
index 5bfc180d4d58e..a3cdde9bde1ac 100644
--- a/.gitignore
+++ b/.gitignore
@@ -26,6 +26,8 @@ library/target
 *.rmeta
 *.mir
 Cargo.lock
+/doc/mdbook-metrics/target
+*.png
 
 ## Temporary files
 *~
@@ -46,7 +48,6 @@ package-lock.json
 ## Kani
 *.out
 
-
 # Added by cargo
 #
 # already existing elements were commented out
diff --git a/doc/book.toml b/doc/book.toml
index 078022e148f1f..9cb0a205ad086 100644
--- a/doc/book.toml
+++ b/doc/book.toml
@@ -19,5 +19,11 @@ runnable = false
 
 [output.linkcheck]
 
+[preprocessor.metrics]
+# Note that the manifest-path is doc/mdbook-metrics, meaning that to build this book, you need to run "mdbook build doc"
+# rather than "mdbook build" from inside the doc/ directory.
+# We choose the former because our "Build Book" Github workflow runs "mdbook build doc."
+command = "cargo run --manifest-path=doc/mdbook-metrics/Cargo.toml"
+
 [rust]
 edition = "2021"
diff --git a/doc/mdbook-metrics/Cargo.toml b/doc/mdbook-metrics/Cargo.toml
new file mode 100644
index 0000000000000..ba6583c62361d
--- /dev/null
+++ b/doc/mdbook-metrics/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "mdbook-kani-metrics"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+mdbook = { version = "^0.4" }
+serde_json = "1.0.132"
diff --git a/doc/mdbook-metrics/src/main.rs b/doc/mdbook-metrics/src/main.rs
new file mode 100644
index 0000000000000..cd261d241e8c1
--- /dev/null
+++ b/doc/mdbook-metrics/src/main.rs
@@ -0,0 +1,106 @@
+use mdbook::book::{Book, Chapter};
+use mdbook::errors::Error;
+use mdbook::preprocess::{CmdPreprocessor, Preprocessor, PreprocessorContext};
+use mdbook::BookItem;
+use std::{env, io, path::Path, process::Command};
+
+fn main() {
+    let mut args = std::env::args().skip(1);
+    match args.next().as_deref() {
+        Some("supports") => {
+            // Supports all renderers.
+            return;
+        }
+        Some(arg) => {
+            eprintln!("unknown argument: {arg}");
+            std::process::exit(1);
+        }
+        None => {}
+    }
+
+    if let Err(e) = handle_preprocessing() {
+        eprintln!("{}", e);
+        std::process::exit(1);
+    }
+}
+
+// Plot the Kani metrics.
+// The mdbook builder reads the postprocessed book from stdout,
+// so suppress all Command output to avoid having its output interpreted as part of the book
+fn run_kani_metrics_script() -> Result<(), Error> {
+    // This will be the absolute path to the "doc/" folder
+    let original_dir = env::current_dir()?;
+    let tools_path = original_dir.join(Path::new("doc/src/tools"));
+
+    let kani_std_analysis_path = Path::new("scripts/kani-std-analysis");
+    env::set_current_dir(kani_std_analysis_path)?;
+
+    Command::new("pip")
+        .args(&["install", "-r", "requirements.txt"])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    Command::new("python")
+        .args(&[
+            "kani_std_analysis.py",
+            "--plot-only",
+            "--plot-dir",
+            &tools_path.to_string_lossy(),
+        ])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    env::set_current_dir(&original_dir)?;
+
+    Ok(())
+}
+
+struct AddKaniGraphs;
+
+impl Preprocessor for AddKaniGraphs {
+    fn name(&self) -> &str {
+        "add-metrics"
+    }
+
+    fn run(&self, _ctx: &PreprocessorContext, mut book: Book) -> Result<Book, Error> {
+        book.for_each_mut(|item| {
+            if let BookItem::Chapter(ch) = item {
+                if ch.name == "Kani" {
+                    add_graphs(ch);
+                    return;
+                }
+            }
+        });
+        Ok(book)
+    }
+}
+
+fn add_graphs(chapter: &mut Chapter) {
+    let new_content = r#"
+## Kani Metrics
+
+Note that these metrics are for x86-64 architectures.
+
+## `core`
+![Unsafe Metrics](core_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
+
+![Safe Metrics](core_safe_metrics.png)
+"#;
+
+    chapter.content.push_str(new_content);
+}
+
+pub fn handle_preprocessing() -> Result<(), Error> {
+    run_kani_metrics_script()?;
+    let pre = AddKaniGraphs;
+    let (ctx, book) = CmdPreprocessor::parse_input(io::stdin())?;
+
+    let processed_book = pre.run(&ctx, book)?;
+    serde_json::to_writer(io::stdout(), &processed_book)?;
+
+    Ok(())
+}
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index e6b2a9c78e598..59f08d58e63d5 100644
--- a/doc/src/SUMMARY.md
+++ b/doc/src/SUMMARY.md
@@ -9,7 +9,6 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
 
-
 ---
 
 - [Challenges](./challenges.md)
diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
new file mode 100755
index 0000000000000..82050a7e1baf2
--- /dev/null
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -0,0 +1,319 @@
+#!/usr/bin/env python3
+
+import argparse
+from collections import defaultdict
+import csv
+import json
+import sys
+from datetime import datetime
+import matplotlib.pyplot as plt
+import matplotlib.dates as mdates
+from matplotlib.ticker import FixedLocator
+import os
+
+# Output metrics about Kani's application to the standard library by:
+#   1. Postprocessing results from running `kani list`, which collects data about Kani harnesses and contracts.
+#   2. Postprocessing results from std-analysis.sh, which outputs metrics about the standard library unrelated to Kani (e.g., a list of the functions in each crate).
+#   3. Comparing the output of steps #1 and #2 to compare the Kani-verified portion of the standard library to the overall library,
+#      e.g., what fraction of unsafe functions have Kani contracts.
+
+# Notes:
+# - This script assumes that std-analysis.sh and `kani list` have already run, since we expect to invoke this script from `run-kani.sh`.
+# - The results are architecture-dependent: the standard library has functions that are only present for certain architectures, 
+#   and https://github.com/model-checking/verify-rust-std/pull/122 has Kani harnesses that only run on x86-64.
+# - The total functions under contract are not necessarily equal to the sum of unsafe and safe functions under contract.
+#   We've added a few functions (three, as of writing) with contracts to this fork, e.g. ffi::c_str::is_null_terminated.
+#   Since std-analysis.sh runs on the standard library given a toolchain (not this fork), it doesn't know about this function and therefore can't classify it as safe or unsafe.
+#   But `kani list` runs on this fork, so it can still see it and add it to the total functions under contract.
+# - See #TODOs for known limitations.
+
+# Process the results from Kani's std-analysis.sh script for each crate.
+# TODO For now, we just handle "core", but we should process all crates in the library.
+class GenericSTDMetrics():
+    def __init__(self, results_dir):
+        self.results_directory = results_dir
+        self.unsafe_fns_count = 0
+        self.safe_abstractions_count = 0
+        self.safe_fns_count = 0
+        self.unsafe_fns = []
+        self.safe_abstractions = []
+        self.safe_fns = [] 
+
+        self.read_std_analysis()
+        
+    # Read {crate}_overall_counts.csv
+    # and return the number of unsafe functions and safe abstractions
+    def read_overall_counts(self):
+        file_path = f"{self.results_directory}/core_scan_overall.csv"
+        with open(file_path, 'r') as f:
+            csv_reader = csv.reader(f, delimiter=';')
+            counts = {row[0]: int(row[1]) for row in csv_reader if len(row) >= 2}
+        self.unsafe_fns_count = counts.get('unsafe_fns', 0)
+        self.safe_abstractions_count = counts.get('safe_abstractions', 0)
+        self.safe_fns_count = counts.get('safe_fns', 0)
+
+    # Read {crate}_scan_functions.csv
+    # and return an array of the unsafe functions and the safe abstractions
+    def read_scan_functions(self):
+        expected_header_start = "name;is_unsafe;has_unsafe_ops"
+        file_path = f"{self.results_directory}/core_scan_functions.csv"
+
+        with open(file_path, 'r') as f:
+            csv_reader = csv.reader(f, delimiter=';', quotechar='"')
+            
+            # The row parsing logic below assumes the column structure in expected_header_start,
+            # so assert that is how the header begins before continuing
+            header = next(csv_reader)
+            header_str = ';'.join(header[:3])
+            if not header_str.startswith(expected_header_start):
+                print(f"Error: Unexpected CSV header in {file_path}")
+                print(f"Expected header to start with: {expected_header_start}")
+                print(f"Actual header: {header_str}")
+                sys.exit(1)
+
+            for row in csv_reader:
+                if len(row) >= 3:
+                    name, is_unsafe, has_unsafe_ops = row[0], row[1], row[2]
+                    # An unsafe function is a function for which is_unsafe=true
+                    if is_unsafe.strip() == "true":
+                        self.unsafe_fns.append(name)
+                    else:
+                        assert is_unsafe.strip() == "false" # sanity check against malformed data
+                        self.safe_fns.append(name)
+                        # A safe abstraction is a safe function with unsafe ops
+                        if has_unsafe_ops.strip() == "true":
+                            self.safe_abstractions.append(name)
+
+    def read_std_analysis(self):
+        self.read_overall_counts()
+        self.read_scan_functions()
+
+        # Sanity checks
+        if len(self.unsafe_fns) != self.unsafe_fns_count:
+            print(f"Number of unsafe functions does not match core_scan_functions.csv")
+            print(f"UNSAFE_FNS_COUNT: {self.unsafe_fns_count}")
+            print(f"UNSAFE_FNS length: {len(self.unsafe_fns)}")
+            sys.exit(1)
+
+        if len(self.safe_abstractions) != self.safe_abstractions_count:
+            print(f"Number of safe abstractions does not match core_scan_functions.csv")
+            print(f"SAFE_ABSTRACTIONS_COUNT: {self.safe_abstractions_count}")
+            print(f"SAFE_ABSTRACTIONS length: {len(self.safe_abstractions)}")
+            sys.exit(1)
+        
+        if len(self.safe_fns) != self.safe_fns_count:
+            print(f"Number of safe functions does not match core_scan_functions.csv")
+            print(f"SAFE_FNS_COUNT: {self.safe_fns_count}")
+            print(f"SAFE_FNS length: {len(self.safe_fns)}")
+            sys.exit(1)
+
+# Process the results of running `kani list` against the standard library,
+# i.e., the Kani STD metrics for a single date (whichever day this script is running).
+class KaniListSTDMetrics():
+    def __init__(self, kani_list_filepath):
+        self.total_fns_under_contract = 0
+        # List of (fn, has_harnesses) tuples, where fn is a function under contract and has_harnesses=true iff the contract has at least one harness
+        self.fns_under_contract = []
+        self.expected_kani_list_version = "0.1"
+
+        self.read_kani_list_data(kani_list_filepath)
+
+    def read_kani_list_data(self, kani_list_filepath):
+        try:
+            with open(kani_list_filepath, 'r') as f:
+                kani_list_data = json.load(f)
+        except FileNotFoundError:
+            print(f"Kani list JSON file not found.")
+            sys.exit(1)
+        
+        if kani_list_data.get("file-version") != self.expected_kani_list_version:
+            print(f"Kani list JSON file version does not match expected version {self.expected_kani_list_version}")
+            sys.exit(1)
+
+        for contract in kani_list_data.get('contracts', []):
+            func_under_contract = contract.get('function', '')
+            has_harnesses = len(contract.get('harnesses', [])) > 0
+            self.fns_under_contract.append((func_under_contract, has_harnesses))
+
+        self.total_fns_under_contract = kani_list_data.get('totals', {}).get('functions-under-contract', 0)
+
+# Generate metrics about Kani's application to the standard library over time
+# by reading past metrics from metrics_file, then computing today's metrics.
+class KaniSTDMetricsOverTime():
+    def __init__(self, metrics_file):
+        self.dates = []
+        self.unsafe_metrics = ['total_unsafe_fns', 'unsafe_fns_under_contract', 'verified_unsafe_fns_under_contract']
+        self.safe_abstr_metrics = ['total_safe_abstractions', 'safe_abstractions_under_contract', 'verified_safe_abstractions_under_contract']
+        self.safe_metrics = ['total_safe_fns', 'safe_fns_under_contract', 'verified_safe_fns_under_contract']
+        # The keys in these dictionaries are unsafe_metrics, safe_abstr_metrics, and safe_metrics, respectively; see update_plot_metrics()
+        self.unsafe_plot_data = defaultdict(list)
+        self.safe_abstr_plot_data = defaultdict(list)
+        self.safe_plot_data = defaultdict(list)
+
+        self.date = datetime.today().date()
+        self.metrics_file = metrics_file
+
+        self.read_historical_data()
+
+    # Read historical data from self.metrics_file and initialize the date range.    
+    def read_historical_data(self):
+        try:
+            with open(self.metrics_file, 'r') as f:
+                all_data = json.load(f)["results"]
+                self.update_plot_metrics(all_data)
+        except FileNotFoundError:
+            all_data = {}
+        
+        self.dates = [datetime.strptime(data["date"], '%Y-%m-%d').date() for data in all_data]
+    
+    # TODO For now, we don't plot how many of the contracts have been verified, since the line overlaps with how many are under contract.
+    # If we want to plot this data, we should probably generate separate plots.
+    # Update the plot data with the provided data.
+    def update_plot_metrics(self, all_data):
+        for data in all_data:
+            for metric in self.unsafe_metrics:
+                if not metric.startswith("verified"):
+                    self.unsafe_plot_data[metric].append(data[metric])
+        
+            for metric in self.safe_abstr_metrics:
+                if not metric.startswith("verified"):
+                    self.safe_abstr_plot_data[metric].append(data[metric])
+            
+            for metric in self.safe_metrics:
+                if not metric.startswith("verified"):
+                    self.safe_plot_data[metric].append(data[metric])
+
+    # Read output from kani list and std-analysis.sh, then compare their outputs to compute Kani-specific metrics
+    # and write the results to {self.metrics_file}
+    def compute_metrics(self, kani_list_filepath, analysis_results_dir):
+        self.dates.append(self.date)
+
+        # Process the `kani list` and `std-analysis.sh` data
+        kani_data = KaniListSTDMetrics(kani_list_filepath)
+        generic_metrics = GenericSTDMetrics(analysis_results_dir)
+
+        print("Comparing kani-list output to std-analysis.sh output and computing metrics...")
+
+        (unsafe_fns_under_contract, verified_unsafe_fns_under_contract) = (0, 0)
+        (safe_abstractions_under_contract, verified_safe_abstractions_under_contract) = (0, 0)
+        (safe_fns_under_contract, verified_safe_fns_under_contract) = (0, 0)
+
+        for (func_under_contract, has_harnesses) in kani_data.fns_under_contract:
+            if func_under_contract in generic_metrics.unsafe_fns:
+                unsafe_fns_under_contract += 1
+                if has_harnesses:
+                    verified_unsafe_fns_under_contract += 1
+            if func_under_contract in generic_metrics.safe_abstractions:
+                safe_abstractions_under_contract += 1
+                if has_harnesses:
+                    verified_safe_abstractions_under_contract += 1
+            if func_under_contract in generic_metrics.safe_fns:
+                safe_fns_under_contract += 1
+                if has_harnesses:
+                    verified_safe_fns_under_contract += 1
+
+        # Keep the keys here in sync with unsafe_metrics, safe_metrics, and safe_abstr_metrics
+        data = {
+            "date": self.date,
+            "total_unsafe_fns": generic_metrics.unsafe_fns_count,
+            "total_safe_abstractions": generic_metrics.safe_abstractions_count,
+            "total_safe_fns": generic_metrics.safe_fns_count,
+            "unsafe_fns_under_contract": unsafe_fns_under_contract,
+            "verified_unsafe_fns_under_contract": verified_unsafe_fns_under_contract,
+            "safe_abstractions_under_contract": safe_abstractions_under_contract,
+            "verified_safe_abstractions_under_contract": verified_safe_abstractions_under_contract,
+            "safe_fns_under_contract": safe_fns_under_contract,
+            "verified_safe_fns_under_contract": verified_safe_fns_under_contract,
+            "total_functions_under_contract": kani_data.total_fns_under_contract,
+        }
+
+        self.update_plot_metrics([data])
+
+        # Update self.metrics_file so that these results are included in our historical data for next time
+        with open(self.metrics_file, 'r') as f:
+            content = json.load(f)
+            content["results"].append(data)
+        
+        with open(self.metrics_file, 'w') as f:
+            json.dump(content, f, indent=2, default=str)
+        
+        print(f"Wrote metrics data for date {self.date} to {self.metrics_file}")    
+
+    # Make a single plot with specified data, title, and filename
+    def plot_single(self, data, title, filename, plot_dir):
+        plt.figure(figsize=(14, 8))
+
+        colors = ['#1f77b4', '#ff7f0e', '#2ca02c', '#d62728', '#946F7bd', '#8c564b', '#e377c2', '#7f7f7f', '#bcbd22', '#17becf']
+        
+        for i, (metric, values) in enumerate(data.items()):
+            color = colors[i % len(colors)]
+            plt.plot(self.dates, values, 'o-', color=color, label=metric, markersize=6)
+            
+            # Mark each point on the line with the y value
+            for x, y in zip(self.dates, values):
+                plt.annotate(str(y), 
+                            (mdates.date2num(x), y), 
+                            xytext=(0, 5), 
+                            textcoords='offset points',
+                            ha='center', 
+                            va='bottom',
+                            color=color,
+                            fontweight='bold')
+
+        plt.title(title)
+        plt.xlabel("Date")
+        plt.ylabel("Count")
+        
+        # Set x-axis to only show ticks for the dates we have
+        plt.gca().xaxis.set_major_locator(FixedLocator(mdates.date2num(self.dates)))
+        plt.gca().xaxis.set_major_formatter(mdates.DateFormatter('%Y-%m-%d'))
+        
+        plt.gcf().autofmt_xdate()
+        plt.tight_layout()
+        plt.legend(bbox_to_anchor=(1.05, 1), loc='upper left')
+        
+        outfile = os.path.join(plot_dir, filename)
+
+        plt.savefig(outfile, bbox_inches='tight', dpi=300)
+        plt.close()
+
+        print(f"PNG graph generated: {outfile}")
+
+    def plot(self, plot_dir):
+        self.plot_single(self.unsafe_plot_data, title="Contracts on Unsafe Functions in core", filename="core_unsafe_metrics.png", plot_dir=plot_dir)
+        self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", filename="core_safe_abstractions_metrics.png", plot_dir=plot_dir)
+        self.plot_single(self.safe_plot_data, title="Contracts on Safe Functions in core", filename="core_safe_metrics.png", plot_dir=plot_dir)
+
+def main():
+    parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.")
+    parser.add_argument('--metrics-file', 
+                    type=str, 
+                    default="metrics-data.json", 
+                    help="Path to the JSON file containing metrics data (default: metrics-data.json)")
+    parser.add_argument('--kani-list-file', 
+                    type=str, 
+                    default="kani-list.json", 
+                    help="Path to the JSON file containing the Kani list data (default: kani-list.json)")
+    # The default is /tmp/std_lib_analysis/results because, as of writing, that's always where std-analysis.sh outputs its results.
+    parser.add_argument('--analysis-results-dir', 
+                    type=str, 
+                    default="/tmp/std_lib_analysis/results", 
+                    help="Path to the folder file containing the std-analysis.sh results (default: /tmp/std_lib_analysis/results)")
+    parser.add_argument('--plot-only', 
+                    action='store_true',
+                    help="Instead of computing the metrics, just read existing metrics from --metrics-file and plot the results.")
+    parser.add_argument('--plot-dir',
+                        default=".",
+                        help="Path to the folder where the plots should be saved (default: current directory). Only used if --plot-only is provided.")
+    
+    args = parser.parse_args()
+
+    metrics = KaniSTDMetricsOverTime(args.metrics_file)
+
+    if args.plot_only:
+        metrics.plot(args.plot_dir)
+    else:
+        metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)
+
+if __name__ == "__main__":
+    main()
diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json
new file mode 100644
index 0000000000000..75a71c0301483
--- /dev/null
+++ b/scripts/kani-std-analysis/metrics-data.json
@@ -0,0 +1,17 @@
+{
+  "results": [
+    {
+      "date": "2025-01-01",
+      "total_unsafe_fns": 6987,
+      "total_safe_abstractions": 1704,
+      "total_safe_fns": 14666,
+      "unsafe_fns_under_contract": 144,
+      "verified_unsafe_fns_under_contract": 132,
+      "safe_abstractions_under_contract": 41,
+      "verified_safe_abstractions_under_contract": 41,
+      "safe_fns_under_contract": 77,
+      "verified_safe_fns_under_contract": 77,
+      "total_functions_under_contract": 224
+    }
+  ]
+}
\ No newline at end of file
diff --git a/scripts/kani-std-analysis/requirements.txt b/scripts/kani-std-analysis/requirements.txt
new file mode 100644
index 0000000000000..6ccafc3f904ba
--- /dev/null
+++ b/scripts/kani-std-analysis/requirements.txt
@@ -0,0 +1 @@
+matplotlib
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 72aa8ef176056..234b2fda9e0f3 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -7,7 +7,7 @@ usage() {
     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 "  --run <verify-std|list>  Optional: Specify whether to run 'verify-std' or 'list' command. Defaults to 'verify-std' if not specified."
+    echo "  --run <verify-std|list|metrics>  Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, or collect Kani-specific metrics. Defaults to 'verify-std' if not specified."
     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
 }
@@ -34,11 +34,11 @@ while [[ $# -gt 0 ]]; do
             fi
             ;;
         --run)
-            if [[ -n $2 && ($2 == "verify-std" || $2 == "list") ]]; then
+            if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics") ]]; then
                 run_command=$2
                 shift 2
             else
-                echo "Error: Invalid run command. Must be 'verify-std' or 'list'."
+                echo "Error: Invalid run command. Must be 'verify-std', 'list', or 'metrics'."
                 usage
             fi
             ;;
@@ -296,6 +296,20 @@ main() {
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format markdown
+    elif [[ "$run_command" == "metrics" ]]; then
+        local current_dir=$(pwd)
+        echo "Running Kani list command..."
+        "$kani_path" list -Z list $unstable_args ./library --std --format json
+        echo "Running Kani's std-analysis command..."
+        pushd $build_dir
+        ./scripts/std-analysis.sh
+        popd
+        pushd scripts/kani-std-analysis
+        pip install -r requirements.txt
+        echo "Computing Kani-specific metrics..."
+        ./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json
+        popd
+        rm kani-list.json
     fi
 }