diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 13e1321d6494..2a0123929b4a 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -242,6 +242,11 @@ pub struct VerificationArgs {
     #[arg(long)]
     pub default_unwind: Option<u32>,
 
+    /// Output the verification results to a JSON file at the specified path.
+    /// This feature is unstable and it requires `-Z unstable-options` to be used
+    #[arg(long)]
+    pub export_json: Option<PathBuf>,
+
     /// When specified, the harness filter will only match the exact fully qualified name of a harness
     #[arg(long, requires("harnesses"))]
     pub exact: bool,
@@ -734,6 +739,12 @@ impl ValidateArgs for VerificationArgs {
                 UnstableFeature::UnstableOptions,
             )?;
 
+            self.common_args.check_unstable(
+                self.export_json.is_some(),
+                "export-json",
+                UnstableFeature::UnstableOptions,
+            )?;
+
             Ok(())
         };
 
@@ -777,6 +788,15 @@ impl ValidateArgs for VerificationArgs {
                     "Conflicting options: --sarif isn't compatible with --output-format=old.",
                 ));
             }
+            // `--output-format=old` bypasses CBMC's structured output entirely: `run_cbmc` mocks a
+            // result with no properties, and treats a timeout as success. An export produced from
+            // that would be indistinguishable from a real clean run.
+            if self.export_json.is_some() && self.output_format == OutputFormat::Old {
+                return Err(Error::raw(
+                    ErrorKind::ArgumentConflict,
+                    "Conflicting options: --export-json isn't compatible with --output-format=old.",
+                ));
+            }
             if self.concrete_playback.is_some() && self.jobs().will_multithread() {
                 // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called.
                 return Err(Error::raw(
@@ -790,6 +810,19 @@ impl ValidateArgs for VerificationArgs {
                     "Conflicting options: --sarif isn't compatible with --only-codegen.",
                 ));
             }
+            // Neither code-generation-only mode runs verification, so there is nothing to export.
+            // `--only-codegen` would otherwise succeed without writing the file the user asked for,
+            // and `--no-codegen` would write a document describing a run that never happened.
+            if self.export_json.is_some() && (self.only_codegen || self.no_codegen) {
+                let incompatible =
+                    if self.only_codegen { "--only-codegen" } else { "--no-codegen" };
+                return Err(Error::raw(
+                    ErrorKind::ArgumentConflict,
+                    format!(
+                        "Conflicting options: --export-json isn't compatible with {incompatible}."
+                    ),
+                ));
+            }
             if self.jobs().will_multithread() && self.output_format != OutputFormat::Terse {
                 // More verbose output formats make it hard to interpret output right now when run in parallel.
                 // This can be removed when we change up how results are printed.
@@ -1133,6 +1166,32 @@ mod tests {
         check_unstable_flag!("--no-slice-formula", no_slice_formula);
     }
 
+    #[test]
+    fn check_export_json_conflicts() {
+        expect_validation_error(
+            "kani file.rs -Z unstable-options --export-json out.json --output-format=old",
+            ErrorKind::ArgumentConflict,
+        );
+        expect_validation_error(
+            "kani file.rs -Z unstable-options --export-json out.json --only-codegen",
+            ErrorKind::ArgumentConflict,
+        );
+        expect_validation_error(
+            "kani file.rs -Z unstable-options --export-json out.json --no-codegen",
+            ErrorKind::ArgumentConflict,
+        );
+    }
+
+    #[test]
+    fn check_export_json_unstable() {
+        check_opt!(
+            "--export-json results.json",
+            Some(UnstableFeature::UnstableOptions),
+            export_json,
+            Some(PathBuf::from("results.json"))
+        );
+    }
+
     #[test]
     fn check_concrete_playback_unstable() {
         let check = |input: &str| {
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 6891d49fd66a..dc4ae72b2db6 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -18,7 +18,7 @@ use tokio::process::Command as TokioCommand;
 use crate::args::common::Verbosity;
 use crate::args::{OutputFormat, VerificationArgs};
 use crate::cbmc_output_parser::{
-    CheckStatus, Property, VerificationOutput, extract_results, process_cbmc_output,
+    CheckStatus, ParserItem, Property, VerificationOutput, extract_results, process_cbmc_output,
 };
 use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
 use crate::coverage::cov_results::{CoverageCheck, CoverageResults};
@@ -26,6 +26,141 @@ use crate::coverage::cov_results::{CoverageRegion, CoverageTerm};
 use crate::session::KaniSession;
 use crate::util::render_command;
 
+/// CBMC version and system information
+#[derive(Debug, Clone)]
+pub struct CbmcInfo {
+    pub version: String,
+    pub os_info: String,
+}
+
+/// CBMC runtime and execution statistics
+#[derive(Debug, Clone, Default)]
+pub struct CbmcStats {
+    pub runtime_symex_s: Option<f64>,
+    pub size_program_expression: Option<u32>,
+    pub slicing_removed_assignments: Option<u32>,
+    pub vccs_generated: Option<u32>,
+    pub vccs_remaining: Option<u32>,
+    pub runtime_postprocess_equation_s: Option<f64>,
+    pub runtime_convert_ssa_s: Option<f64>,
+    pub runtime_post_process_s: Option<f64>,
+    pub runtime_solver_s: Option<f64>,
+    pub runtime_decision_procedure_s: Option<f64>,
+}
+
+impl KaniSession {
+    /// Get CBMC version and system information
+    pub fn get_cbmc_info(&self) -> Result<CbmcInfo> {
+        let output = std::process::Command::new("cbmc")
+            .arg("--version")
+            .output()
+            .map_err(|_| anyhow::Error::msg("Failed to run cbmc --version"))?;
+
+        let version_output = String::from_utf8_lossy(&output.stdout);
+        let lines: Vec<&str> = version_output.lines().collect();
+
+        // Extract version from first line (e.g., "6.7.1 (cbmc-6.7.1)")
+        let version = lines
+            .first()
+            .and_then(|line| line.split_whitespace().next())
+            .unwrap_or("unknown")
+            .to_string();
+
+        // For OS info, we'll use the system information since CBMC --version doesn't provide it
+        let os_info = format!(
+            "{} {} {}",
+            std::env::consts::ARCH,
+            std::env::consts::OS,
+            std::env::consts::FAMILY
+        );
+
+        Ok(CbmcInfo { version, os_info })
+    }
+}
+
+/// Collect the statistics CBMC reports for a single verification run.
+///
+/// CBMC reports these as free-text status messages. `--json-ui`, which Kani always passes, wraps
+/// each message in a JSON envelope carrying `messageType` and `messageText`, but it does not break
+/// the numbers out into fields of their own, so the message text remains the only source available
+/// (CBMC's `structured_datat` mechanism, which would render as real JSON fields, is not used by
+/// these call sites). What the envelope does buy us is the ability to require a status message and
+/// to anchor on CBMC's exact label, rather than searching arbitrary output for a loose pattern.
+///
+/// Returns `None` when no message carried statistics, which is the case whenever CBMC did not get
+/// far enough to report any.
+fn merge_cbmc_stats(items: &[ParserItem]) -> Option<CbmcStats> {
+    let mut stats = CbmcStats::default();
+    let mut found_any = false;
+
+    for item in items {
+        if let ParserItem::Message { message_text, message_type } = item
+            && message_type == "STATUS-MESSAGE"
+        {
+            found_any |= record_cbmc_stat(message_text, &mut stats);
+        }
+    }
+
+    found_any.then_some(stats)
+}
+
+/// Record the statistic a single CBMC status message carries, if it carries one. Later messages win,
+/// matching CBMC's own behaviour of reporting a running figure more than once.
+/// Returns whether this message was recognized.
+fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
+    // "Generated 1 VCC(s), 1 remaining after simplification"
+    if let Some(counts) = message
+        .strip_prefix("Generated ")
+        .and_then(|rest| rest.strip_suffix(" remaining after simplification"))
+        && let Some((generated, remaining)) = counts.split_once(" VCC(s), ")
+    {
+        stats.vccs_generated = generated.parse().ok();
+        stats.vccs_remaining = remaining.parse().ok();
+        return stats.vccs_generated.is_some() || stats.vccs_remaining.is_some();
+    }
+
+    // "slicing removed 81 assignments", or "simple slicing removed 5 assignments" when only the
+    // simple slicer ran. CBMC emits one or the other; our schema has a single field for both.
+    if let Some(rest) = message.strip_suffix(" assignments")
+        && let Some(count) = rest
+            .strip_prefix("slicing removed ")
+            .or_else(|| rest.strip_prefix("simple slicing removed "))
+    {
+        stats.slicing_removed_assignments = count.parse().ok();
+        return stats.slicing_removed_assignments.is_some();
+    }
+
+    // Everything else is reported as "<label>: <value>".
+    let Some((label, value)) = message.split_once(": ") else {
+        return false;
+    };
+    match label {
+        // "150 steps"
+        "size of program expression" => {
+            stats.size_program_expression =
+                value.strip_suffix(" steps").and_then(|steps| steps.parse().ok());
+            stats.size_program_expression.is_some()
+        }
+        "Runtime Symex" => record_seconds(value, &mut stats.runtime_symex_s),
+        "Runtime Postprocess Equation" => {
+            record_seconds(value, &mut stats.runtime_postprocess_equation_s)
+        }
+        "Runtime Convert SSA" => record_seconds(value, &mut stats.runtime_convert_ssa_s),
+        "Runtime Post-process" => record_seconds(value, &mut stats.runtime_post_process_s),
+        "Runtime Solver" => record_seconds(value, &mut stats.runtime_solver_s),
+        "Runtime decision procedure" => {
+            record_seconds(value, &mut stats.runtime_decision_procedure_s)
+        }
+        _ => false,
+    }
+}
+
+/// Record a duration CBMC reports as "0.00408627s" or "1.5416e-05s".
+fn record_seconds(value: &str, field: &mut Option<f64>) -> bool {
+    *field = value.strip_suffix('s').and_then(|seconds| seconds.parse().ok());
+    field.is_some()
+}
+
 /// We will use Cadical by default since it performed better than MiniSAT in our analysis.
 /// Note: Kissat was marginally better, but it is an external solver which could be more unstable.
 static DEFAULT_SOLVER: CbmcSolver = CbmcSolver::Cadical;
@@ -77,6 +212,8 @@ pub struct VerificationResult {
     pub generated_concrete_test: bool,
     /// The coverage results
     pub coverage_results: Option<CoverageResults>,
+    /// CBMC execution statistics extracted from messages
+    pub cbmc_stats: Option<CbmcStats>,
 }
 
 impl KaniSession {
@@ -149,7 +286,12 @@ impl KaniSession {
 
         if let Ok(output) = res {
             // The timeout wasn't reached
-            Ok(VerificationResult::from(output?, harness.attributes.should_panic, start_time))
+            Ok(VerificationResult::from(
+                output?,
+                harness.attributes.should_panic,
+                start_time,
+                self.args.export_json.is_some(),
+            ))
         } else {
             // An error occurs if the timeout was reached
 
@@ -163,6 +305,7 @@ impl KaniSession {
                 runtime: start_time.elapsed(),
                 generated_concrete_test: false,
                 coverage_results: None,
+                cbmc_stats: None,
             })
         }
     }
@@ -274,19 +417,22 @@ impl KaniSession {
         args
     }
 
+    /// The solver this run will actually use for a harness: `--solver` takes precedence over the
+    /// harness attribute, which takes precedence over the default.
+    ///
+    /// Anything reporting the configuration of a run must resolve it through here rather than
+    /// reading the harness attribute directly, or it will describe a different run than the one
+    /// `handle_solver_args` builds.
+    pub fn resolved_solver<'a>(&'a self, harness_solver: &'a Option<CbmcSolver>) -> &'a CbmcSolver {
+        self.args.solver.as_ref().or(harness_solver.as_ref()).unwrap_or(&DEFAULT_SOLVER)
+    }
+
     pub fn handle_solver_args(
         &self,
         harness_solver: &Option<CbmcSolver>,
         args: &mut Vec<OsString>,
     ) -> Result<()> {
-        let solver = if let Some(solver) = &self.args.solver {
-            // `--solver` option takes precedence over attributes
-            solver
-        } else if let Some(solver) = harness_solver {
-            solver
-        } else {
-            &DEFAULT_SOLVER
-        };
+        let solver = self.resolved_solver(harness_solver);
 
         match solver {
             CbmcSolver::Bitwuzla => {
@@ -336,9 +482,14 @@ impl VerificationResult {
         output: VerificationOutput,
         should_panic: bool,
         start_time: Instant,
+        collect_cbmc_stats: bool,
     ) -> VerificationResult {
         let runtime = start_time.elapsed();
-        let (_, results) = extract_results(output.processed_items);
+        let (remaining_items, results) = extract_results(output.processed_items);
+
+        // Only `--export-json` consumes these, and collecting them means running several regexes
+        // over every message CBMC emitted, so skip the work entirely when nothing will read it.
+        let cbmc_stats = if collect_cbmc_stats { merge_cbmc_stats(&remaining_items) } else { None };
 
         if let Some(results) = results {
             let (status, failed_properties) =
@@ -351,6 +502,7 @@ impl VerificationResult {
                 runtime,
                 generated_concrete_test: false,
                 coverage_results,
+                cbmc_stats,
             }
         } else {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
@@ -366,6 +518,7 @@ impl VerificationResult {
                 runtime,
                 generated_concrete_test: false,
                 coverage_results: None,
+                cbmc_stats,
             }
         }
     }
@@ -378,6 +531,7 @@ impl VerificationResult {
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
             coverage_results: None,
+            cbmc_stats: None,
         }
     }
 
@@ -392,6 +546,7 @@ impl VerificationResult {
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
             coverage_results: None,
+            cbmc_stats: None,
         }
     }
 
@@ -570,6 +725,74 @@ mod tests {
 
     use super::*;
 
+    /// The statistics messages below are verbatim CBMC 6.x `--json-ui` output, so a CBMC change to
+    /// any of these labels shows up here as a test failure rather than as silently missing data.
+    #[test]
+    fn check_cbmc_stats_from_status_messages() {
+        let messages = [
+            "Runtime Symex: 0.00049675s",
+            "size of program expression: 21 steps",
+            "simple slicing removed 5 assignments",
+            "Generated 1 VCC(s), 1 remaining after simplification",
+            "Runtime Postprocess Equation: 1.5416e-05s",
+            "Runtime Convert SSA: 0.00012525s",
+            "Runtime Post-process: 2.0292e-05s",
+            "Runtime Solver: 4.1167e-05s",
+            "Runtime decision procedure: 0.000193542s",
+        ];
+        let items: Vec<ParserItem> = messages
+            .iter()
+            .map(|text| ParserItem::Message {
+                message_text: text.to_string(),
+                message_type: "STATUS-MESSAGE".to_string(),
+            })
+            .collect();
+
+        let stats = merge_cbmc_stats(&items).expect("statistics should be recognized");
+        assert_eq!(stats.runtime_symex_s, Some(0.00049675));
+        assert_eq!(stats.size_program_expression, Some(21));
+        assert_eq!(stats.slicing_removed_assignments, Some(5));
+        assert_eq!(stats.vccs_generated, Some(1));
+        assert_eq!(stats.vccs_remaining, Some(1));
+        assert_eq!(stats.runtime_postprocess_equation_s, Some(1.5416e-05));
+        assert_eq!(stats.runtime_convert_ssa_s, Some(0.00012525));
+        assert_eq!(stats.runtime_post_process_s, Some(2.0292e-05));
+        assert_eq!(stats.runtime_solver_s, Some(4.1167e-05));
+        assert_eq!(stats.runtime_decision_procedure_s, Some(0.000193542));
+    }
+
+    /// The full slicer reports without the "simple" prefix.
+    #[test]
+    fn check_cbmc_stats_full_slicer() {
+        let mut stats = CbmcStats::default();
+        assert!(record_cbmc_stat("slicing removed 81 assignments", &mut stats));
+        assert_eq!(stats.slicing_removed_assignments, Some(81));
+    }
+
+    /// Anchoring on the label is what the message type and exact-match parsing buy us: text that
+    /// merely mentions a statistic, or that CBMC reports as a warning rather than a status message,
+    /// must not be mistaken for a measurement.
+    #[test]
+    fn check_cbmc_stats_ignore_unrelated_text() {
+        let mut stats = CbmcStats::default();
+        assert!(!record_cbmc_stat("assertion failed: Runtime Solver: 1s is too slow", &mut stats));
+        assert!(!record_cbmc_stat("Runtime Solver: not-a-number", &mut stats));
+        assert!(!record_cbmc_stat("VERIFICATION FAILED", &mut stats));
+        assert_eq!(stats.runtime_solver_s, None);
+
+        let warning = [ParserItem::Message {
+            message_text: "Runtime Solver: 4.1167e-05s".to_string(),
+            message_type: "WARNING".to_string(),
+        }];
+        assert!(merge_cbmc_stats(&warning).is_none());
+    }
+
+    /// No statistics at all (CBMC died early, or verbosity hid them) must not fabricate a record.
+    #[test]
+    fn check_cbmc_stats_absent() {
+        assert!(merge_cbmc_stats(&[]).is_none());
+    }
+
     #[test]
     fn check_resolve_unwind_value() {
         // Command line unwind value for specific harnesses take precedence over default annotation value
diff --git a/kani-driver/src/frontend/json_handler.rs b/kani-driver/src/frontend/json_handler.rs
new file mode 100644
index 000000000000..f9214ab73437
--- /dev/null
+++ b/kani-driver/src/frontend/json_handler.rs
@@ -0,0 +1,51 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use serde_json::{Value, json};
+use std::path::PathBuf;
+
+/// A handler for building and exporting JSON data structures.
+///
+/// `JsonHandler` provides a convenient interface for constructing JSON objects,
+/// adding key-value pairs, appending to arrays, and exporting the final result
+/// to a file.
+pub struct JsonHandler {
+    /// The JSON data being constructed.
+    pub(crate) data: Value,
+    /// Optional path where the JSON data will be exported.
+    export_path: Option<PathBuf>,
+}
+
+impl JsonHandler {
+    /// Creates a new `JsonHandler` with an optional export path.
+    /// If `export_path` is `None`, calls to `export()` will be no-ops.
+    pub fn new(export_path: Option<PathBuf>) -> Self {
+        Self { data: json!({}), export_path }
+    }
+
+    /// Adds or updates a key-value pair in the JSON object.
+    /// If the key already exists, its value will be overwritten.
+    pub fn add_item(&mut self, key: &str, value: Value) {
+        self.data[key] = value;
+    }
+
+    /// Appends a value to the array at the specified key.
+    /// Creates a new array if the key doesn't exist or is null.
+    /// Panics if the key exists but is not an array or null.
+    pub fn add_harness_detail(&mut self, key: &str, value: Value) {
+        if self.data[key].is_null() {
+            self.data[key] = json!([]);
+        }
+        self.data[key].as_array_mut().unwrap().push(value);
+    }
+
+    /// Exports the JSON data to the configured file path with pretty-printing.
+    /// Returns an error if the file cannot be written.
+    pub fn export(&self) -> Result<(), std::io::Error> {
+        if let Some(path) = &self.export_path {
+            std::fs::write(path, serde_json::to_string_pretty(&self.data)?)
+        } else {
+            Ok(())
+        }
+    }
+}
diff --git a/kani-driver/src/frontend/mod.rs b/kani-driver/src/frontend/mod.rs
new file mode 100644
index 000000000000..61431fb24ffc
--- /dev/null
+++ b/kani-driver/src/frontend/mod.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Frontend module for handling different output formats and JSON generation
+//! This module separates the JSON handling logic from the main verification logic
+
+pub mod json_handler;
+pub mod schema_utils;
+
+pub use json_handler::JsonHandler;
+pub use schema_utils::*;
+
+#[cfg(test)]
+mod tests;
diff --git a/kani-driver/src/frontend/schema_utils.rs b/kani-driver/src/frontend/schema_utils.rs
new file mode 100644
index 000000000000..2984f640b004
--- /dev/null
+++ b/kani-driver/src/frontend/schema_utils.rs
@@ -0,0 +1,531 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Utility functions for creating structured JSON schemas
+// This module contains helper functions to convert Kani internal structures to JSON
+
+use crate::call_cbmc::VerificationStatus;
+use crate::cbmc_output_parser::{CheckStatus, Property};
+use crate::frontend::JsonHandler;
+use crate::harness_runner::HarnessResult;
+use crate::project::Project;
+use crate::session::KaniSession;
+use anyhow::Result;
+use kani_metadata::{CbmcSolver, HarnessMetadata};
+use serde::Serialize;
+use serde_json::{Value, json};
+use std::collections::BTreeMap;
+use std::ffi::OsStr;
+use std::process::Command;
+use time::OffsetDateTime;
+use time::format_description::well_known::Rfc3339;
+
+/// Creates structured JSON metadata for an export run
+/// This utility function captures basic environment for the whole session
+pub fn create_metadata_json() -> Value {
+    let timestamp = OffsetDateTime::now_utc()
+        .format(&Rfc3339)
+        .unwrap_or_else(|_| "1970-01-01T00:00:00Z".to_string());
+
+    let kani_version = env!("CARGO_PKG_VERSION");
+    let target = env!("TARGET");
+    let build_mode = if cfg!(debug_assertions) { "debug" } else { "release" };
+
+    json!({
+    "version": "1.0",
+    "timestamp": timestamp,
+    "kani_version": kani_version,
+    "target": target,
+    "build_mode": build_mode,
+    })
+}
+
+/// Ask a tool for its version, returning the first line of its `--version` output.
+///
+/// Returns `None` if the tool cannot be run or says nothing: a version we could not determine is
+/// reported as null rather than guessed, and never fails the run.
+fn tool_version(binary: &OsStr) -> Option<String> {
+    let output = Command::new(binary).arg("--version").output().ok()?;
+    let stdout = String::from_utf8_lossy(&output.stdout);
+    let first_line = stdout.lines().next()?.trim();
+    (!first_line.is_empty()).then(|| first_line.to_string())
+}
+
+/// The version of every tool this run relies on, addressing part of
+/// <https://github.com/model-checking/kani/issues/942>'s sibling request
+/// <https://github.com/model-checking/kani/issues/2572>.
+///
+/// A key is present only if the run uses that tool, so an absent key means "not part of this run"
+/// while a present null means "used, but its version could not be determined". The versions are
+/// verbatim first lines of `--version` output, so they are display strings rather than parseable
+/// values.
+///
+/// This spawns a process per tool. That is only paid when `--export-json` is requested, and once per
+/// run rather than per harness.
+pub fn create_tool_versions_json(session: &KaniSession, harnesses: &[&HarnessMetadata]) -> Value {
+    let mut tools = serde_json::Map::new();
+
+    tools.insert("kani".to_string(), json!(env!("CARGO_PKG_VERSION")));
+
+    // `kani-compiler` is a rustc driver, so `--version` reports the toolchain it was built against.
+    // That is the version that decides how Rust is translated, which makes it the interesting one.
+    // Asking the binary beats reading a `rustc` from PATH, which need not be the same toolchain.
+    tools.insert("rustc".to_string(), json!(tool_version(session.kani_compiler.as_os_str())));
+
+    // The CBMC suite. `cbmc` and `goto-cc` run for every verification; `goto-instrument` runs to
+    // instrument the goto program; `goto-synthesizer` only for loop-contract synthesis.
+    for (key, binary) in
+        [("cbmc", "cbmc"), ("goto_cc", "goto-cc"), ("goto_instrument", "goto-instrument")]
+    {
+        tools.insert(key.to_string(), json!(tool_version(OsStr::new(binary))));
+    }
+    if session.args.synthesize_loop_contracts {
+        tools.insert(
+            "goto_synthesizer".to_string(),
+            json!(tool_version(OsStr::new("goto-synthesizer"))),
+        );
+    }
+
+    // Solvers, which can differ per harness, so this is every distinct solver the run resolves to.
+    // A list rather than a map keyed by name, because the set varies per run and consumers should
+    // not have to discover which keys might appear. Only solvers CBMC invokes as separate binaries
+    // have a version of their own: CaDiCaL and MiniSAT are built into CBMC and would report its
+    // version, so they are named with a null version rather than given a misleading one.
+    let mut solvers = BTreeMap::new();
+    for harness in harnesses {
+        let solver = effective_solver(session, &harness.attributes.solver);
+        // A run whose solver CBMC chooses for itself names no solver to report.
+        let Some(name) = solver.name else { continue };
+        // Probe each binary once, however many harnesses use it. Ordered by name so two runs with
+        // the same solvers produce the same document.
+        solvers
+            .entry(name)
+            .or_insert_with(|| solver.binary.and_then(|binary| tool_version(OsStr::new(&binary))));
+    }
+    tools.insert(
+        "solvers".to_string(),
+        json!(
+            solvers
+                .into_iter()
+                .map(|(name, version)| json!({"name": name, "version": version}))
+                .collect::<Vec<_>>()
+        ),
+    );
+
+    Value::Object(tools)
+}
+
+/// Every property of a harness, counted by status.
+///
+/// The counts partition the properties exhaustively, so
+/// `passed + failed + unreachable + undetermined + error + satisfied + unsatisfiable + covered +
+/// uncovered == total_properties` always holds. Counting only a few statuses meant the numbers
+/// silently failed to reconcile whenever a run had cover statements, coverage properties, or a
+/// solver error, and a consumer had no way to tell that from a run where they genuinely summed.
+///
+/// The match below is deliberately exhaustive: a new `CheckStatus` should fail to compile here
+/// rather than quietly go uncounted.
+#[derive(Default)]
+struct PropertyCounts {
+    passed: usize,
+    failed: usize,
+    unreachable: usize,
+    undetermined: usize,
+    error: usize,
+    satisfied: usize,
+    unsatisfiable: usize,
+    covered: usize,
+    uncovered: usize,
+}
+
+impl PropertyCounts {
+    fn of(properties: &[Property]) -> Self {
+        let mut counts = Self::default();
+        for property in properties {
+            let counter = match property.status {
+                CheckStatus::Success => &mut counts.passed,
+                CheckStatus::Failure => &mut counts.failed,
+                CheckStatus::Unreachable => &mut counts.unreachable,
+                // Kani renders both of these as UNDETERMINED, so they are grouped here to keep the
+                // export agreeing with the text output. CBMC 6+ reports UNKNOWN when another
+                // property's failure makes this one impossible to conclude either way.
+                CheckStatus::Undetermined | CheckStatus::Unknown => &mut counts.undetermined,
+                CheckStatus::Error => &mut counts.error,
+                CheckStatus::Satisfied => &mut counts.satisfied,
+                CheckStatus::Unsatisfiable => &mut counts.unsatisfiable,
+                CheckStatus::Covered => &mut counts.covered,
+                CheckStatus::Uncovered => &mut counts.uncovered,
+            };
+            *counter += 1;
+        }
+        counts
+    }
+
+    fn to_json(&self) -> Value {
+        json!({
+            "total_properties": self.passed + self.failed + self.unreachable + self.undetermined
+                + self.error + self.satisfied + self.unsatisfiable + self.covered + self.uncovered,
+            "passed": self.passed,
+            "failed": self.failed,
+            "unreachable": self.unreachable,
+            "undetermined": self.undetermined,
+            "solver_error": self.error,
+            "satisfied": self.satisfied,
+            "unsatisfiable": self.unsatisfiable,
+            "covered": self.covered,
+            "uncovered": self.uncovered,
+        })
+    }
+
+    /// The same shape, for a harness whose properties were never measured.
+    fn unmeasured_json() -> Value {
+        json!({
+            "total_properties": null,
+            "passed": null,
+            "failed": null,
+            "unreachable": null,
+            "undetermined": null,
+            "solver_error": null,
+            "satisfied": null,
+            "unsatisfiable": null,
+            "covered": null,
+            "uncovered": null,
+            "error": "Could not extract property details due to verification failure"
+        })
+    }
+}
+
+/// Creates structured JSON metadata for the project
+/// This utility function captures detailed info for the project
+pub fn create_project_metadata_json(project: &Project) -> Value {
+    json!({
+    "crate_name": project.metadata.iter()
+    .map(|m| m.crate_name.clone())
+    .collect::<Vec<String>>(),
+    // The real workspace root, which only exists for Cargo projects; null for a standalone run.
+    // `Project::outdir` is the compiler output directory -- for Cargo it sits under
+    // `target/<triple>/debug/deps` -- so reporting it as the workspace root was simply wrong.
+    "workspace_root": project.cargo_metadata.as_ref()
+    .map(|metadata| metadata.workspace_root.clone()),
+    "output_dir": project.outdir.clone(),
+    })
+}
+/// Creates structured JSON metadata for a harness
+/// This utility function separates harness metadata creation from the main verification logic
+pub fn create_harness_metadata_json(h: &HarnessMetadata) -> Value {
+    json!({
+        "pretty_name": h.pretty_name, // use this as identifier
+        "mangled_name": h.mangled_name,
+        "crate_name": h.crate_name,
+        "source": {
+            "file": h.original_file,
+            "start_line": h.original_start_line,
+            "end_line": h.original_end_line
+        },
+        "goto_file": h.goto_file.as_ref().map(|p| p.to_string_lossy().to_string()),
+        "attributes": {
+            "kind": format!("{:?}", h.attributes.kind),
+            "should_panic": h.attributes.should_panic,
+        },
+        "contract":{
+            "contracted_function_name": h.contract.as_ref()
+            .map(|c| c.contracted_function_name.as_str()),
+            "recursion_tracker": h.contract.as_ref()
+            .and_then(|c| c.recursion_tracker.as_ref()),
+        },
+        "has_loop_contracts": h.has_loop_contracts,
+        "is_automatically_generated": h.is_automatically_generated,
+
+    })
+}
+
+/// Creates verification result JSON with harness reference
+/// This reduces duplication between harness metadata and verification results
+pub fn create_verification_result_json(result: &HarnessResult) -> Value {
+    // Extract detailed verification results as "checks"
+    let checks = match &result.result.results {
+        Ok(properties) => properties
+            .iter()
+            .enumerate()
+            .map(|(i, prop)| {
+                json!({
+                    "id": i + 1,
+                    "function": prop.property_id.fn_name.as_deref().unwrap_or("unknown"),
+                    "status": format!("{:?}", prop.status),
+                    "description": prop.description,
+                    "location": {
+                        "file": prop.source_location.file.as_deref().unwrap_or("unknown"),
+                        "line": prop.source_location.line.as_deref().unwrap_or("unknown"),
+                        "column": prop.source_location.column.as_deref().unwrap_or("unknown"),
+                    },
+                    "category": prop.property_id.class,
+                })
+            })
+            .collect::<Vec<_>>(),
+        Err(_) => vec![],
+    };
+
+    json!({
+        "harness_id": result.harness.pretty_name,  // Reference to harness instead of duplicating name
+        "status": match result.result.status {
+            VerificationStatus::Success => "Success",
+            VerificationStatus::Failure => "Failure",
+        },
+        "duration_ms": (result.result.runtime.as_millis() as u64),
+        "checks": checks,
+    })
+}
+
+/// Creates a verification summary with clean structure
+pub fn create_verification_summary_json(
+    results: &[HarnessResult],
+    selected: usize,
+    status_label: &str,
+) -> Value {
+    let successful =
+        results.iter().filter(|r| r.result.status == VerificationStatus::Success).count();
+    let failed = results.len() - successful;
+    let total_duration_ms: u64 = results.iter().map(|r| r.result.runtime.as_millis() as u64).sum();
+
+    let verification_results: Vec<_> =
+        results.iter().map(|r| create_verification_result_json(r)).collect();
+
+    json!({
+        "summary": {
+            "total_harnesses": selected,
+            "executed": results.len(),
+            "status": status_label,
+            "successful": successful,
+            "failed": failed,
+            "duration_ms": total_duration_ms
+        },
+        "results": verification_results
+    })
+}
+
+/// Helper function to add verification results to JsonHandler
+/// This utility function encapsulates the logic for adding verification summary to JSON output
+pub fn add_runner_results_to_json(
+    handler: &mut JsonHandler,
+    results: &[HarnessResult],
+    selected: usize,
+    status_label: &str,
+) {
+    // Use frontend utility to create structured verification summary
+    let summary = create_verification_summary_json(results, selected, status_label);
+    handler.add_item("verification_results", summary);
+}
+
+/// Process harness results and enrich JSON handler with additional metadata.
+/// This function handles the complex harness processing logic, combining verification results
+/// with harness metadata to create enriched JSON output.
+pub fn process_harness_results(
+    handler: &mut JsonHandler,
+    harnesses: &[&HarnessMetadata],
+    results: &[HarnessResult],
+) -> Result<()> {
+    // The main verification results are handled by the harness runner
+    for h in harnesses {
+        let harness_result = results.iter().find(|r| r.harness.pretty_name == h.pretty_name);
+
+        // Add error details for this harness. This accumulates one entry per harness, keyed by
+        // `harness_id`, the same way the `cbmc` array does: a single top-level object would let a
+        // later successful harness overwrite an earlier failure, and report a run containing a
+        // failing harness as having no errors at all.
+        if let Some(result) = harness_result {
+            handler.add_harness_detail("error_details", match result.result.status {
+                VerificationStatus::Failure => {
+                    json!({
+                        "harness_id": h.pretty_name,
+                        "has_errors": true,
+                        "error_type": match result.result.failed_properties {
+                            crate::call_cbmc::FailedProperties::None => "unknown_failure",
+                            crate::call_cbmc::FailedProperties::PanicsOnly => "assertion_failure",
+                            crate::call_cbmc::FailedProperties::Other => "verification_failure",
+                            crate::call_cbmc::FailedProperties::Error => "property_error",
+                        },
+                        "failed_properties_type": format!("{:?}", result.result.failed_properties),
+                        "exit_status": match &result.result.results {
+                            Err(crate::call_cbmc::ExitStatus::Timeout) => "timeout".to_string(),
+                            Err(crate::call_cbmc::ExitStatus::OutOfMemory) => "out_of_memory".to_string(),
+                            Err(crate::call_cbmc::ExitStatus::Other(code)) => format!("exit_code_{}", code),
+                            Ok(_) => "properties_failed".to_string()
+                        }
+                    })
+                },
+                VerificationStatus::Success => json!({
+                    "harness_id": h.pretty_name,
+                    "has_errors": false
+                })
+            });
+
+            // Add property details for this harness. `harness_id` is what makes an entry
+            // attributable: this array is built in harness-metadata order while
+            // `verification_results.results` is in completion order, so the two cannot be
+            // correlated by position.
+            handler.add_harness_detail(
+                "property_details",
+                json!({
+                    "harness_id": h.pretty_name,
+                    "property_details": match &result.result.results {
+                        Ok(properties) => PropertyCounts::of(properties).to_json(),
+                        // CBMC produced no property results at all (timeout, out of memory, crash).
+                        // Keep every count present so the shape does not change between runs, and
+                        // report them as null: `0` would assert that nothing failed, when the truth is
+                        // that nothing was measured.
+                        Err(_) => PropertyCounts::unmeasured_json()
+                    }
+                }),
+            );
+        }
+    }
+
+    Ok(())
+}
+
+/// The solver CBMC will actually run with.
+struct EffectiveSolver {
+    /// Display name, or `None` when the choice is left to CBMC -- `--smt2` on its own names no
+    /// solver, and a wrong name is worse than no name.
+    name: Option<String>,
+    /// The binary to ask for a version, when CBMC runs the solver as a separate process. `None` for
+    /// solvers built into CBMC, which would report CBMC's own version rather than one of their own.
+    binary: Option<String>,
+}
+
+/// Resolve the solver for a harness, applying every layer that can select one.
+///
+/// `KaniSession::resolved_solver` covers `--solver`, the harness attribute and the default, but
+/// `--cbmc-args` is appended *after* Kani's own solver flags and CBMC takes the last one it sees, so
+/// a solver named there overrides all three. Everything that reports a solver must go through here,
+/// or the run's own metadata ends up contradicting itself.
+fn effective_solver(session: &KaniSession, harness_solver: &Option<CbmcSolver>) -> EffectiveSolver {
+    let mut override_seen = false;
+    let mut resolved = EffectiveSolver { name: None, binary: None };
+    let mut cbmc_args = session.args.cbmc_args.iter();
+    while let Some(arg) = cbmc_args.next() {
+        // Last one wins, matching CBMC.
+        let (name, binary) = match arg.to_str() {
+            // `--sat-solver` selects a solver built into CBMC, so there is no binary to probe.
+            Some("--sat-solver") => {
+                (cbmc_args.next().and_then(|name| name.to_str()).map(str::to_string), None)
+            }
+            Some("--external-sat-solver") => {
+                let binary = cbmc_args.next().and_then(|name| name.to_str()).map(str::to_string);
+                (binary.clone(), binary)
+            }
+            Some("--bitwuzla") => (Some("bitwuzla".to_string()), Some("bitwuzla".to_string())),
+            Some("--cvc5") => (Some("cvc5".to_string()), Some("cvc5".to_string())),
+            Some("--z3") => (Some("z3".to_string()), Some("z3".to_string())),
+            // `--smt2` alone leaves the choice of SMT solver to CBMC.
+            Some("--smt2") => (None, None),
+            _ => continue,
+        };
+        override_seen = true;
+        resolved = EffectiveSolver { name, binary };
+    }
+
+    if override_seen {
+        return resolved;
+    }
+
+    let (name, binary) = match session.resolved_solver(harness_solver) {
+        CbmcSolver::Bitwuzla => ("bitwuzla", Some("bitwuzla")),
+        CbmcSolver::Cadical => ("cadical", None),
+        CbmcSolver::Cvc5 => ("cvc5", Some("cvc5")),
+        CbmcSolver::Kissat => ("kissat", Some("kissat")),
+        CbmcSolver::Minisat => ("minisat", None),
+        CbmcSolver::Z3 => ("z3", Some("z3")),
+        CbmcSolver::Binary(binary) => (binary.as_str(), Some(binary.as_str())),
+    };
+    EffectiveSolver { name: Some(name.to_string()), binary: binary.map(str::to_string) }
+}
+
+/// The `--object-bits` value CBMC will actually run with.
+///
+/// `VerificationArgs::cbmc_object_bits` reports nothing once the user supplies `--object-bits`
+/// through `--cbmc-args`, because Kani then stops passing its own default. That is the right answer
+/// for building the command line and the wrong one for describing it: the run does have a value, so
+/// take it from `--cbmc-args` instead of exporting null for an explicitly configured run.
+fn effective_object_bits(session: &KaniSession) -> Option<u32> {
+    if let Some(bits) = session.args.cbmc_object_bits() {
+        return Some(bits);
+    }
+    let mut cbmc_args = session.args.cbmc_args.iter();
+    while let Some(arg) = cbmc_args.next() {
+        if arg == "--object-bits" {
+            return cbmc_args.next().and_then(|bits| bits.to_str()?.parse().ok());
+        }
+    }
+    None
+}
+
+pub fn process_cbmc_results(
+    handler: &mut JsonHandler,
+    harnesses: &[&HarnessMetadata],
+    results: &[HarnessResult],
+    session: &KaniSession,
+) -> Result<()> {
+    let cbmc_info_opt = session.get_cbmc_info().ok();
+    for h in harnesses {
+        let harness_result = results.iter().find(|r| r.harness.pretty_name == h.pretty_name);
+        handler.add_harness_detail("cbmc", json!({
+            // basic name for harnesses
+            "harness_id": h.pretty_name,
+
+            // Per-harness CBMC info (key-value pairs) without parsing CBMC stdout
+            "cbmc_metadata": {
+                // Version / OS info (same for all harnesses in a run)
+                "version": cbmc_info_opt.as_ref().map(|i| i.version.clone()),
+                "os_info": cbmc_info_opt.as_ref().map(|i| i.os_info.clone()),
+            },
+            // Configuration passed to CBMC for this harness. Both values are resolved the same way
+            // the CBMC command line itself resolves them, so that a consumer reading this is
+            // reading the run that actually happened.
+            "configuration": {
+                "object_bits": effective_object_bits(session),
+                "solver": effective_solver(session, &h.attributes.solver).name,
+            },
+
+            // CBMC execution statistics extracted from messages
+            "cbmc_stats": harness_result.and_then(|r| r.result.cbmc_stats.as_ref()).map(|s| json!({
+            "runtime_symex_s": s.runtime_symex_s,
+            "size_program_expression": s.size_program_expression,
+            "slicing_removed_assignments": s.slicing_removed_assignments,
+            "vccs_generated": s.vccs_generated,
+            "vccs_remaining": s.vccs_remaining,
+            "runtime_postprocess_equation_s": s.runtime_postprocess_equation_s,
+            "runtime_convert_ssa_s": s.runtime_convert_ssa_s,
+            "runtime_post_process_s": s.runtime_post_process_s,
+            "runtime_solver_s": s.runtime_solver_s,
+            "runtime_decision_procedure_s": s.runtime_decision_procedure_s
+            }))
+        }));
+    }
+    Ok(())
+}
+
+/// Simple container to standardize tool outputs captured during verification
+#[derive(Serialize)]
+#[allow(dead_code)]
+pub struct ToolOutput<'a> {
+    /// Arbitrary tool name key under which this output will be grouped
+    pub tool: &'a str,
+    /// Harness identifier this output belongs to
+    pub harness_id: &'a str,
+    /// Unparsed stdout text emitted by the tool
+    pub stdout: &'a str,
+}
+
+/// Add a tool output entry to the JSON under a tool-named array
+#[allow(dead_code)]
+pub fn add_tool_output(handler: &mut JsonHandler, output: ToolOutput<'_>) {
+    // structure: top-level key is the tool name, value is an array of entries
+    handler.add_harness_detail(
+        output.tool,
+        json!({
+            "harness_id": output.harness_id,
+            "stdout": output.stdout,
+        }),
+    );
+}
diff --git a/kani-driver/src/frontend/tests/mod.rs b/kani-driver/src/frontend/tests/mod.rs
new file mode 100644
index 000000000000..cb53347d30eb
--- /dev/null
+++ b/kani-driver/src/frontend/tests/mod.rs
@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Tests for the frontend module
+//! This module contains tests for the schema_utils module
+//! and the json_handler module
+
+#[cfg(test)]
+mod schema_utils_test;
diff --git a/kani-driver/src/frontend/tests/schema_utils_test.rs b/kani-driver/src/frontend/tests/schema_utils_test.rs
new file mode 100644
index 000000000000..f1693cad5a14
--- /dev/null
+++ b/kani-driver/src/frontend/tests/schema_utils_test.rs
@@ -0,0 +1,222 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// Tests for the schema_utils module
+/// This module contains tests for the schema_utils module
+/// and the json_handler module
+use crate::call_cbmc::{ExitStatus, FailedProperties, VerificationResult, VerificationStatus};
+use crate::cbmc_output_parser::{CheckStatus, Property, PropertyId, SourceLocation};
+use crate::frontend::JsonHandler;
+use crate::frontend::schema_utils::{
+    add_runner_results_to_json, create_harness_metadata_json, create_metadata_json,
+    create_project_metadata_json, create_verification_result_json,
+    create_verification_summary_json,
+};
+use crate::harness_runner::HarnessResult;
+use crate::project::Project;
+use kani_metadata::{HarnessAttributes, HarnessKind, HarnessMetadata, KaniMetadata};
+use std::path::PathBuf;
+use std::time::Duration;
+#[test]
+fn test_create_metadata_json() {
+    let json = create_metadata_json();
+
+    assert!(json.is_object());
+    assert_eq!(json["version"], "1.0");
+    assert!(json["timestamp"].as_str().unwrap().contains('T'));
+    assert!(["debug", "release"].contains(&json["build_mode"].as_str().unwrap()));
+}
+
+#[test]
+fn test_create_project_metadata_json() {
+    let mut project = Project::default();
+    let metadata = KaniMetadata {
+        crate_name: "sample_crate".to_string(),
+        proof_harnesses: vec![],
+        test_harnesses: vec![],
+        unsupported_features: vec![],
+        contracted_functions: vec![],
+        autoharness_md: None,
+    };
+    project.outdir = PathBuf::from("/tmp/outdir");
+    project.metadata.push(metadata);
+
+    let json = create_project_metadata_json(&project);
+    assert_eq!(json["crate_name"][0], "sample_crate");
+    assert_eq!(json["output_dir"], "/tmp/outdir");
+    // No Cargo metadata on a standalone project, so there is no workspace root to report.
+    assert!(json["workspace_root"].is_null());
+}
+
+#[test]
+fn test_create_harness_metadata_json() {
+    let harness = HarnessMetadata {
+        pretty_name: "crate::mod::my_harness".to_string(),
+        mangled_name: "mangled::harness".to_string(),
+        crate_name: "sample_crate".to_string(),
+        original_file: "src/lib.rs".to_string(),
+        original_start_line: 10,
+        original_end_line: 20,
+        goto_file: Some(PathBuf::from("target/goto_file.goto")),
+        attributes: HarnessAttributes::new(HarnessKind::Proof),
+        contract: None,
+        has_loop_contracts: true,
+        is_automatically_generated: false,
+    };
+
+    let json = create_harness_metadata_json(&harness);
+
+    assert_eq!(json["pretty_name"], "crate::mod::my_harness");
+    assert_eq!(json["crate_name"], "sample_crate");
+    assert_eq!(json["source"]["file"], "src/lib.rs");
+    assert_eq!(json["source"]["start_line"], 10);
+    assert_eq!(json["source"]["end_line"], 20);
+    assert_eq!(json["has_loop_contracts"], true);
+    assert_eq!(json["is_automatically_generated"], false);
+}
+
+#[test]
+fn test_create_verification_result_json() {
+    let harness = HarnessMetadata {
+        pretty_name: "crate::my_harness".to_string(),
+        mangled_name: "mangled_name".to_string(),
+        crate_name: "sample_crate".to_string(),
+        original_file: "src/lib.rs".to_string(),
+        original_start_line: 1,
+        original_end_line: 2,
+        goto_file: None,
+        attributes: HarnessAttributes::new(HarnessKind::Proof),
+        contract: None,
+        has_loop_contracts: false,
+        is_automatically_generated: false,
+    };
+
+    let properties = vec![
+        Property {
+            property_id: PropertyId {
+                id: 1,
+                fn_name: Some("foo".to_string()),
+                class: "safety".to_string(),
+            },
+            status: CheckStatus::Success,
+            description: "no overflow".to_string(),
+            source_location: SourceLocation {
+                file: Some("src/lib.rs".to_string()),
+                function: Some("foo".to_string()),
+                line: Some("42".to_string()),
+                column: Some("5".to_string()),
+            },
+            reach: None,
+            trace: None,
+        },
+        Property {
+            property_id: PropertyId {
+                id: 2,
+                fn_name: Some("bar".to_string()),
+                class: "assertion".to_string(),
+            },
+            status: CheckStatus::Failure,
+            description: "assert failed".to_string(),
+            source_location: SourceLocation {
+                file: Some("src/main.rs".to_string()),
+                function: Some("bar".to_string()),
+                line: Some("10".to_string()),
+                column: Some("3".to_string()),
+            },
+            reach: None,
+            trace: None,
+        },
+    ];
+
+    let verification_result = VerificationResult {
+        status: VerificationStatus::Failure,
+        failed_properties: FailedProperties::Other,
+        results: Ok(properties),
+        runtime: Duration::from_millis(120),
+        generated_concrete_test: false,
+        coverage_results: None,
+        cbmc_stats: None,
+    };
+
+    let harness_result = HarnessResult { harness: &harness, result: verification_result };
+
+    let json = create_verification_result_json(&harness_result);
+
+    // --- Assertions ---
+    assert_eq!(json["harness_id"], "crate::my_harness");
+    assert_eq!(json["status"], "Failure");
+    assert_eq!(json["checks"][0]["function"], "foo");
+    assert_eq!(json["checks"][1]["function"], "bar");
+    assert_eq!(json["checks"][1]["location"]["file"], "src/main.rs");
+
+    // Optional extra check
+    assert!(json["duration_ms"].as_u64().unwrap() >= 100);
+}
+
+#[test]
+fn test_create_verification_summary_json_real() {
+    // Create a real harness
+    let harness = HarnessMetadata {
+        pretty_name: "foo::harness_ok".into(),
+        mangled_name: "foo_harness_ok".into(),
+        crate_name: "sample".into(),
+        original_file: "src/lib.rs".into(),
+        original_start_line: 10,
+        original_end_line: 20,
+        goto_file: None,
+        attributes: HarnessAttributes::new(HarnessKind::Proof),
+        contract: None,
+        has_loop_contracts: false,
+        is_automatically_generated: false,
+    };
+
+    // Create a VerificationResult
+    let verification_result = VerificationResult::mock_success();
+
+    let harness_result = HarnessResult { harness: &harness, result: verification_result };
+
+    let json = create_verification_summary_json(&[harness_result], 1, "Completed");
+
+    assert_eq!(json["summary"]["status"], "Completed");
+    assert_eq!(json["summary"]["total_harnesses"], 1);
+    assert_eq!(json["summary"]["executed"], 1);
+    assert_eq!(json["summary"]["successful"], 1);
+    assert_eq!(json["summary"]["failed"], 0);
+    assert!(json["results"].is_array());
+}
+
+#[test]
+fn test_add_runner_results_to_json_real() {
+    let harness = HarnessMetadata {
+        pretty_name: "bar::harness_fail".into(),
+        mangled_name: "bar_harness_fail".into(),
+        crate_name: "sample".into(),
+        original_file: "src/main.rs".into(),
+        original_start_line: 5,
+        original_end_line: 15,
+        goto_file: None,
+        attributes: HarnessAttributes::new(HarnessKind::Proof),
+        contract: None,
+        has_loop_contracts: false,
+        is_automatically_generated: false,
+    };
+
+    let verification_result = VerificationResult {
+        status: VerificationStatus::Failure,
+        failed_properties: FailedProperties::Other,
+        results: Err(ExitStatus::Other(42)),
+        runtime: Duration::from_millis(120),
+        generated_concrete_test: false,
+        coverage_results: None,
+        cbmc_stats: None,
+    };
+
+    let harness_result = HarnessResult { harness: &harness, result: verification_result };
+
+    let mut handler = JsonHandler::new(None);
+    add_runner_results_to_json(&mut handler, &[harness_result], 1, "Failed");
+
+    let summary = &handler.data["verification_results"]["summary"];
+    assert_eq!(summary["status"], "Failed");
+    assert_eq!(summary["failed"], 1);
+}
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index a5d028637e77..d3c05c0face1 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -10,6 +10,7 @@ use std::path::Path;
 
 use crate::args::{NumThreads, OutputFormat};
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
+use crate::frontend::{JsonHandler, schema_utils::add_runner_results_to_json};
 use crate::project::Project;
 use crate::session::{BUG_REPORT_URL, KaniSession};
 
@@ -54,6 +55,7 @@ impl<'pr> HarnessRunner<'_, 'pr> {
     pub(crate) fn check_all_harnesses(
         &self,
         harnesses: &'pr [&HarnessMetadata],
+        mut json_handler: Option<&mut JsonHandler>,
     ) -> Result<Vec<HarnessResult<'pr>>> {
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
         let pool = {
@@ -98,14 +100,30 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                 .collect::<Result<Vec<_>>>()
         });
         match results {
-            Ok(results) => Ok(results),
+            Ok(results) => {
+                if let Some(handler) = json_handler.as_deref_mut() {
+                    add_runner_results_to_json(handler, &results, harnesses.len(), "completed");
+                }
+                Ok(results)
+            }
             Err(err) => {
                 if err.is::<FailFastHarnessInfo>() {
                     let failed = err.downcast::<FailFastHarnessInfo>().unwrap();
-                    Ok(vec![HarnessResult {
+                    let result = vec![HarnessResult {
                         harness: sorted_harnesses[failed.index_to_failing_harness],
                         result: failed.result,
-                    }])
+                    }];
+
+                    if let Some(handler) = json_handler {
+                        add_runner_results_to_json(
+                            handler,
+                            &result,
+                            harnesses.len(),
+                            "completed_with_fail_fast",
+                        );
+                    }
+
+                    Ok(result)
                 } else {
                     Err(err)
                 }
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index f497c3a4cf3f..22aad350eb4a 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -12,11 +12,16 @@ use args_toml::join_args;
 
 use crate::args::StandaloneSubcommand;
 use crate::concrete_playback::playback::{playback_cargo, playback_standalone};
+use crate::frontend::{
+    JsonHandler, create_harness_metadata_json, create_metadata_json, create_project_metadata_json,
+    create_tool_versions_json, process_cbmc_results, process_harness_results,
+};
 use crate::list::collect_metadata::{list_cargo, list_standalone};
 use crate::project::Project;
 use crate::session::KaniSession;
 use crate::version::print_kani_version;
 use clap::Parser;
+use serde_json::json;
 use tracing::debug;
 
 mod args;
@@ -36,6 +41,8 @@ mod harness_runner;
 mod list;
 mod metadata;
 mod project;
+
+mod frontend;
 mod sarif;
 mod session;
 mod util;
@@ -136,12 +143,42 @@ fn standalone_main() -> Result<()> {
 /// Run verification on the given project.
 fn verify_project(project: Project, session: KaniSession) -> Result<()> {
     debug!(?project, "verify_project");
+    // Only build the JSON document when `--export-json` asks for one. Everything below it is
+    // overhead for every other run, including a `cbmc --version` probe in `process_cbmc_results`.
+    let mut handler =
+        session.args.export_json.as_ref().map(|path| JsonHandler::new(Some(path.clone())));
     let harnesses = session.determine_targets(project.get_all_harnesses())?;
     debug!(n = harnesses.len(), ?harnesses, "verify_project");
 
+    if let Some(handler) = handler.as_mut() {
+        // Add project and export run metadata using frontend utility
+        handler.add_item("metadata", create_metadata_json());
+        handler.add_item("project", create_project_metadata_json(&project));
+        handler.add_item("tools", create_tool_versions_json(&session, &harnesses));
+
+        // The per-harness arrays are filled in lazily below and by the harness runner, so declare
+        // them up front. A run with no matching harnesses would otherwise omit them entirely and
+        // write a document missing four of its documented keys -- and the "no harnesses matched"
+        // error is only reported after the export, so a consumer sees the malformed file first.
+        for key in ["harness_metadata", "error_details", "property_details", "cbmc"] {
+            handler.add_item(key, json!([]));
+        }
+
+        // Add harness metadata using frontend utility
+        for h in &harnesses {
+            handler.add_harness_detail("harness_metadata", create_harness_metadata_json(h));
+        }
+    }
+
     // Verification
     let runner = harness_runner::HarnessRunner { sess: &session, project: &project };
-    let results = runner.check_all_harnesses(&harnesses)?;
+    let results = runner.check_all_harnesses(&harnesses, handler.as_mut())?;
+
+    if let Some(handler) = handler.as_mut() {
+        // Process harness results and add additional metadata using frontend utility function
+        process_harness_results(handler, &harnesses, &results)?;
+        process_cbmc_results(handler, &harnesses, &results, &session)?;
+    }
 
     if session.args.coverage {
         // We generate a timestamp to save the coverage data in a folder named
@@ -162,6 +199,11 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
         session.save_coverage_results(&project, &results, &timestamp)?;
     }
 
+    if let Some(handler) = handler.as_mut() {
+        handler.add_item("coverage", json!({"enabled": session.args.coverage}));
+        handler.export()?;
+    }
+
     session.write_sarif(&results)?;
     session.print_final_summary(&results)
 }
diff --git a/kani-driver/src/sarif.rs b/kani-driver/src/sarif.rs
index 849c48c7c2db..7c63f5fd36e9 100644
--- a/kani-driver/src/sarif.rs
+++ b/kani-driver/src/sarif.rs
@@ -327,6 +327,7 @@ mod tests {
             runtime: Duration::from_secs(1),
             generated_concrete_test: false,
             coverage_results: None,
+            cbmc_stats: None,
         }
     }
 
@@ -340,6 +341,7 @@ mod tests {
             runtime: Duration::from_secs(1),
             generated_concrete_test: false,
             coverage_results: None,
+            cbmc_stats: None,
         };
         let harness_result = HarnessResult { harness: &harness, result };
 
diff --git a/scripts/ci/copyright-exclude b/scripts/ci/copyright-exclude
index 157d88fbc379..09665d2690d9 100644
--- a/scripts/ci/copyright-exclude
+++ b/scripts/ci/copyright-exclude
@@ -1,6 +1,7 @@
 .clang-format
 .diff
 .ico
+.json
 .md
 .png
 .props
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index 3d875e4919a6..99d8541d7679 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -60,6 +60,7 @@ TESTS=(
     "cargo-coverage cargo-coverage"
     "kani-docs cargo-kani"
     "kani-fixme kani-fixme"
+    "json-handler exec"
 )
 
 # Build compiletest and print configuration. We pick suite / mode combo so there's no test.
diff --git a/scripts/validate_json_export.py b/scripts/validate_json_export.py
new file mode 100755
index 000000000000..22cba5a87453
--- /dev/null
+++ b/scripts/validate_json_export.py
@@ -0,0 +1,249 @@
+#!/usr/bin/env python3
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+"""
+JSON Export Validation Script for Kani Integration Tests
+
+Validates JSON exports against the kani_json_schema.json template.
+"""
+
+import json
+import sys
+import os
+from pathlib import Path
+
+
+def load_schema_template():
+    """Load the JSON schema template"""
+    # Find schema template in tests/json-handler/schema-validation directory
+    script_dir = Path(__file__).parent
+    schema_path = (
+        script_dir.parent
+        / "tests"
+        / "json-handler"
+        / "schema-validation"
+        / "kani_json_schema.json"
+    )
+
+    if not schema_path.exists():
+        print(f"ERROR: Schema template not found at {schema_path}")
+        return None
+
+    with open(schema_path, "r") as f:
+        return json.load(f)
+
+
+def validate_structure_recursive(data, schema, path="", nullable=False):
+    """
+    Recursively validate data structure against schema template.
+
+    Args:
+        data: The JSON data to validate
+        schema: The schema template to validate against
+        path: Current path in the structure (for error messages)
+        nullable: Whether the parent declared this value may be null, via its
+            `_nullable` list. Only such values are allowed to be null where the
+            template expects an object or an array.
+
+    Returns:
+        (success: bool, errors: list)
+    """
+    errors = []
+
+    # A null where the template expects a structure is only acceptable if the parent
+    # declared it nullable; otherwise it is reported below as a type mismatch.
+    if data is None and nullable:
+        return True, errors
+
+    # Handle dict validation
+    if isinstance(schema, dict):
+        if not isinstance(data, dict):
+            # This used to fall through to the leaf case and report success, so an export
+            # with `"metadata": null` bypassed every field required beneath it.
+            errors.append(
+                f"Expected object at {path or '<root>'}, "
+                f"got {type(data).__name__}"
+            )
+            return False, errors
+
+        # Get optional fields list (fields that may or may not be present)
+        optional_fields = schema.get("_optional", [])
+        # Fields whose value may legitimately be null instead of a structure.
+        nullable_fields = schema.get("_nullable", [])
+
+        # All fields in schema are required except metadata fields (starting with _) and optional fields
+        schema_keys = [k for k in schema.keys() if not k.startswith("_")]
+
+        # Check each key in schema
+        for key in schema_keys:
+            # Check if field exists in data
+            if key not in data:
+                # Only report error if field is required (not in optional list)
+                if key not in optional_fields:
+                    current_path = f"{path}.{key}" if path else key
+                    errors.append(f"Missing required field: {current_path}")
+                continue
+
+            # Recursively validate nested structure
+            current_path = f"{path}.{key}" if path else key
+            sub_errors = validate_structure_recursive(
+                data[key], schema[key], current_path, key in nullable_fields
+            )[1]
+            errors.extend(sub_errors)
+
+    # Handle array validation
+    elif isinstance(schema, list) and len(schema) > 0:
+        if not isinstance(data, list):
+            errors.append(f"Expected array at {path}, got {type(data).__name__}")
+        else:
+            # Validate every item against the schema template. Checking only the first
+            # element let malformed data in every later harness pass validation, which
+            # defeats the purpose on exactly the multi-harness runs this validates.
+            for index, item in enumerate(data):
+                sub_errors = validate_structure_recursive(
+                    item, schema[0], f"{path}[{index}]"
+                )[1]
+                errors.extend(sub_errors)
+
+    # Leaf values - no validation needed
+
+    success = len(errors) == 0
+    return success, errors
+
+
+def validate_json_structure(json_file, schema=None):
+    """
+    Validate that JSON export matches the schema template structure.
+    """
+    try:
+        with open(json_file, "r") as f:
+            data = json.load(f)
+    except FileNotFoundError:
+        print(f"ERROR: JSON file {json_file} not found")
+        return False
+    except json.JSONDecodeError as e:
+        print(f"ERROR: Invalid JSON in {json_file}: {e}")
+        return False
+
+    # Load schema if not provided
+    if schema is None:
+        schema = load_schema_template()
+        if schema is None:
+            return False
+
+    # All schema fields are required - validate structure recursively
+    # The recursive validator will catch any missing required fields
+    success, all_errors = validate_structure_recursive(data, schema, "")
+
+    if not success or all_errors:
+        print(f"ERROR: Validation failed for {json_file}:")
+        for error in all_errors:
+            print(f"  - {error}")
+        return False
+
+    print(f"JSON structure validation passed for {json_file}")
+    return True
+
+
+def validate_field_path(json_file, field_path, schema=None):
+    """
+    Validate specific fields at a given path.
+
+    Args:
+        json_file: Path to JSON file
+        field_path: Dot-separated path (e.g., 'metadata', 'verification_results.summary')
+        schema: Optional pre-loaded schema
+    """
+    try:
+        with open(json_file, "r") as f:
+            data = json.load(f)
+    except Exception as e:
+        print(f"ERROR: Failed to load {json_file}: {e}")
+        return False
+
+    # Load schema if not provided
+    if schema is None:
+        schema = load_schema_template()
+        if schema is None:
+            return False
+
+    # Navigate to the field in both data and schema
+    parts = field_path.split(".")
+    current_data = data
+    current_schema = schema
+
+    for part in parts:
+        if part not in current_data:
+            print(
+                f"ERROR: Field path '{field_path}' not found in data. Missing part: '{part}'"
+            )
+            return False
+        current_data = current_data[part]
+
+        if part not in current_schema:
+            print(
+                f"ERROR: Field path '{field_path}' not found in schema template. Missing part: '{part}'"
+            )
+            return False
+        current_schema = current_schema[part]
+
+        # Handle arrays - check first item
+        if isinstance(current_schema, list) and len(current_schema) > 0:
+            current_schema = current_schema[0]
+            if isinstance(current_data, list) and len(current_data) > 0:
+                current_data = current_data[0]
+
+    # Validate structure at this path
+    success, errors = validate_structure_recursive(
+        current_data, current_schema, field_path
+    )
+
+    if not success:
+        print(f"ERROR: Validation failed for {field_path}:")
+        for error in errors:
+            print(f"  - {error}")
+        return False
+
+    print(f"Field validation passed for {field_path}")
+    return True
+
+
+def main():
+    if len(sys.argv) < 2:
+        print(
+            "Usage: python3 validate_json_export.py <json_file> [--field-path <path>]"
+        )
+        sys.exit(1)
+
+    json_file = sys.argv[1]
+
+    # Check if specific field validation requested
+    if len(sys.argv) > 2 and sys.argv[2] == "--field-path":
+        if len(sys.argv) < 4:
+            print("ERROR: --field-path requires a path argument")
+            sys.exit(1)
+
+        field_path = sys.argv[3]
+        if validate_field_path(json_file, field_path):
+            sys.exit(0)
+        else:
+            sys.exit(1)
+
+    # Load schema once
+    schema = load_schema_template()
+    if schema is None:
+        print("ERROR: Could not load schema template")
+        sys.exit(1)
+
+    # Run full validation
+    if validate_json_structure(json_file, schema):
+        print(f"\nAll validations passed for {json_file}")
+        sys.exit(0)
+    else:
+        print(f"\nValidation failed for {json_file}")
+        sys.exit(1)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/tests/.gitignore b/tests/.gitignore
index 814a069a9424..68879fed17a0 100644
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -1,5 +1,6 @@
 # Temporary files and folders
 *.json
+!json-handler/schema-validation/*.json
 kani_concrete_playback
 rmet*/
 target/
diff --git a/tests/json-handler/basic-export/config.yml b/tests/json-handler/basic-export/config.yml
new file mode 100644
index 000000000000..938834ea42cb
--- /dev/null
+++ b/tests/json-handler/basic-export/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: test.sh
+
diff --git a/tests/json-handler/basic-export/test.rs b/tests/json-handler/basic-export/test.rs
new file mode 100644
index 000000000000..1b43dc7373f2
--- /dev/null
+++ b/tests/json-handler/basic-export/test.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --export-json basic_test_output.json
+
+//! Basic test for JSON export functionality
+//! This verifies that the frontend module can export verification results
+
+fn add_numbers(a: u32, b: u32) -> u32 {
+    a + b
+}
+
+#[kani::proof]
+fn verify_add_numbers() {
+    let x: u32 = kani::any();
+    let y: u32 = kani::any();
+    kani::assume(x < 100);
+    kani::assume(y < 100);
+    let result = add_numbers(x, y);
+    assert!(result >= x);
+    assert!(result >= y);
+}
diff --git a/tests/json-handler/basic-export/test.sh b/tests/json-handler/basic-export/test.sh
new file mode 100755
index 000000000000..8e10bd50fe5f
--- /dev/null
+++ b/tests/json-handler/basic-export/test.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test JSON export basic functionality - validates schema_utils.rs functions
+
+set -eu
+# The validator's exit status is piped into `tail` below; without pipefail a failed
+# validation is masked by tail's success and this test passes regardless.
+set -o pipefail
+
+OUTPUT_FILE="test_output.json"
+# Remove the export on every exit path, not just the happy one: a failing
+# validation step exits early under `set -e` and would otherwise leave it behind.
+trap 'rm -f "$OUTPUT_FILE"' EXIT
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+VALIDATOR="$PROJECT_ROOT/scripts/validate_json_export.py"
+
+# Run Kani with JSON export
+kani -Z unstable-options test.rs --export-json "$OUTPUT_FILE"
+
+# Check that JSON file was created
+if [ ! -f "$OUTPUT_FILE" ]; then
+    echo "ERROR: JSON file $OUTPUT_FILE was not created"
+    exit 1
+fi
+
+# Validate JSON structure using the validation script (suppress verbose output)
+python3 "$VALIDATOR" "$OUTPUT_FILE" 2>&1 | tail -1
+
+
diff --git a/tests/json-handler/cargo-export/config.yml b/tests/json-handler/cargo-export/config.yml
new file mode 100644
index 000000000000..927fa124ffc3
--- /dev/null
+++ b/tests/json-handler/cargo-export/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: test.sh
+expected: expected
diff --git a/tests/json-handler/cargo-export/expected b/tests/json-handler/cargo-export/expected
new file mode 100644
index 000000000000..dd4e339c98d9
--- /dev/null
+++ b/tests/json-handler/cargo-export/expected
@@ -0,0 +1 @@
+Cargo export reports the workspace root and the expected harness
diff --git a/tests/json-handler/cargo-export/test.sh b/tests/json-handler/cargo-export/test.sh
new file mode 100755
index 000000000000..520eeab1fbd3
--- /dev/null
+++ b/tests/json-handler/cargo-export/test.sh
@@ -0,0 +1,104 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test JSON export through `cargo kani`. Every other test in this suite drives standalone
+# `kani`, which leaves the Cargo argument handling untested and can never exercise the
+# Cargo-only project metadata: `workspace_root` comes from Cargo metadata and is null for a
+# standalone run, so only this test can tell whether it is reported correctly.
+
+set -eu
+set -o pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+VALIDATOR="$PROJECT_ROOT/scripts/validate_json_export.py"
+
+# Scaffold the crate outside the repository so the build artifacts cannot pollute it.
+WORK_DIR="$(mktemp -d)"
+trap 'rm -rf "$WORK_DIR"' EXIT
+
+mkdir -p "$WORK_DIR/src"
+cat > "$WORK_DIR/Cargo.toml" <<'CARGO'
+[package]
+name = "json_export_cargo_test"
+version = "0.1.0"
+edition = "2021"
+CARGO
+
+cat > "$WORK_DIR/src/lib.rs" <<'RUST'
+#[cfg(kani)]
+#[kani::proof]
+fn check_cargo_export() {
+    let x: u8 = kani::any();
+    kani::assume(x < 10);
+    assert!(x < 20);
+}
+RUST
+
+cd "$WORK_DIR"
+OUTPUT_FILE="$WORK_DIR/cargo_output.json"
+
+cargo kani -Z unstable-options --export-json "$OUTPUT_FILE"
+
+if [ ! -f "$OUTPUT_FILE" ]; then
+    echo "ERROR: JSON file $OUTPUT_FILE was not created"
+    exit 1
+fi
+
+python3 "$VALIDATOR" "$OUTPUT_FILE"
+
+WORK_DIR="$WORK_DIR" python3 << 'EOF_PY'
+import json
+import os
+import sys
+
+with open(os.environ['WORK_DIR'] + '/cargo_output.json', 'r') as f:
+    data = json.load(f)
+
+failures = []
+
+
+def check(condition, message):
+    if not condition:
+        failures.append(message)
+
+
+project = data['project']
+
+# The whole point of this test: a Cargo run must report the crate's workspace root, not the
+# compiler output directory, and the two are different paths.
+expected_root = os.path.realpath(os.environ['WORK_DIR'])
+reported_root = project.get('workspace_root')
+check(reported_root is not None, "workspace_root should not be null for a Cargo project")
+if reported_root is not None:
+    check(os.path.realpath(reported_root) == expected_root,
+          f"workspace_root should be {expected_root}, got {reported_root}")
+
+output_dir = project.get('output_dir')
+check(output_dir is not None, "output_dir should not be null")
+if output_dir is not None and reported_root is not None:
+    check(os.path.realpath(output_dir) != os.path.realpath(reported_root),
+          "output_dir should differ from workspace_root")
+
+check(project.get('crate_name') == ['json_export_cargo_test'],
+      f"unexpected crate_name: {project.get('crate_name')}")
+
+names = [h.get('pretty_name') for h in data['harness_metadata']]
+check(names == ['check_cargo_export'], f"unexpected harnesses: {names}")
+
+summary = data['verification_results']['summary']
+for field, want in [('total_harnesses', 1), ('executed', 1),
+                    ('successful', 1), ('failed', 0)]:
+    check(summary.get(field) == want,
+          f"summary.{field} should be {want}, got {summary.get(field)}")
+
+check(data['tools'].get('kani') is not None, "tools.kani should report a version")
+
+if failures:
+    for failure in failures:
+        print(f"ERROR: {failure}")
+    sys.exit(1)
+
+print("Cargo export reports the workspace root and the expected harness")
+EOF_PY
diff --git a/tests/json-handler/failed-verification/config.yml b/tests/json-handler/failed-verification/config.yml
new file mode 100644
index 000000000000..938834ea42cb
--- /dev/null
+++ b/tests/json-handler/failed-verification/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: test.sh
+
diff --git a/tests/json-handler/failed-verification/test.rs b/tests/json-handler/failed-verification/test.rs
new file mode 100644
index 000000000000..d5c459c09a96
--- /dev/null
+++ b/tests/json-handler/failed-verification/test.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --export-json failed_output.json
+
+//! Test JSON export with failed verification
+//! Verifies that frontend correctly captures failure information in JSON
+
+fn unsafe_subtract(a: u32, b: u32) -> u32 {
+    a - b // This will fail with overflow
+}
+
+#[kani::proof]
+fn verify_unsafe_subtract() {
+    let x: u32 = kani::any();
+    let y: u32 = kani::any();
+    // No assumptions - will trigger overflow
+    let result = unsafe_subtract(x, y);
+    assert!(result <= x); // This will also fail when y > x
+}
diff --git a/tests/json-handler/failed-verification/test.sh b/tests/json-handler/failed-verification/test.sh
new file mode 100755
index 000000000000..a3df8ce0217f
--- /dev/null
+++ b/tests/json-handler/failed-verification/test.sh
@@ -0,0 +1,112 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test JSON export with failed verification - validates error capture
+
+set -eu
+
+OUTPUT_FILE="failed_output.json"
+# Remove the export on every exit path, not just the happy one: a failing
+# validation step exits early under `set -e` and would otherwise leave it behind.
+trap 'rm -f "$OUTPUT_FILE"' EXIT
+
+# Find the project root (where scripts/ directory is)
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+
+# Run Kani with JSON export (expect failure, so don't use -e)
+set +e
+kani -Z unstable-options test.rs --export-json "$OUTPUT_FILE"
+EXIT_CODE=$?
+set -e
+
+# Kani should exit with failure
+if [ $EXIT_CODE -eq 0 ]; then
+    echo "ERROR: Expected Kani to fail but it succeeded"
+    exit 1
+fi
+
+echo "Kani failed as expected"
+
+# Check that JSON file was created despite failure
+if [ ! -f "$OUTPUT_FILE" ]; then
+    echo "ERROR: JSON file $OUTPUT_FILE was not created"
+    exit 1
+fi
+
+echo "JSON file created despite failure"
+
+# Validate that JSON contains failure information
+python3 << 'EOF'
+import json
+import sys
+
+with open('failed_output.json', 'r') as f:
+    data = json.load(f)
+
+# Check verification_results shows failure
+vr = data['verification_results']
+summary = vr['summary']
+
+if summary['successful'] != 0:
+    print(f"ERROR: Expected 0 successful, got {summary['successful']}")
+    sys.exit(1)
+
+if summary['failed'] != 1:
+    print(f"ERROR: Expected 1 failed, got {summary['failed']}")
+    sys.exit(1)
+
+print("Summary shows correct failure count")
+
+# Check that results array contains failure status
+results = vr['results']
+if len(results) != 1:
+    print(f"ERROR: Expected 1 result, got {len(results)}")
+    sys.exit(1)
+
+if results[0]['status'] != 'Failure':
+    print(f"ERROR: Expected status 'Failure', got {results[0]['status']}")
+    sys.exit(1)
+
+print("Result status is 'Failure'")
+
+# Check that error_details exists and has_errors is true
+if 'error_details' not in data:
+    print("ERROR: error_details field missing")
+    sys.exit(1)
+
+# error_details is an array with one entry per harness, each identified by harness_id
+error_details = data['error_details']
+if not isinstance(error_details, list):
+    print(f"ERROR: error_details should be a list, got {type(error_details).__name__}")
+    sys.exit(1)
+
+if len(error_details) != 1:
+    print(f"ERROR: Expected 1 error_details entry, got {len(error_details)}")
+    sys.exit(1)
+
+entry = error_details[0]
+
+if 'harness_id' not in entry:
+    print("ERROR: harness_id field missing")
+    sys.exit(1)
+
+if not entry.get('has_errors'):
+    print("ERROR: has_errors should be true")
+    sys.exit(1)
+
+print("error_details.has_errors is true")
+
+# Verify error_type is present
+if 'error_type' not in entry:
+    print("ERROR: error_type field missing")
+    sys.exit(1)
+
+print("error_type field present")
+
+EOF
+
+echo "All failure validation checks passed!"
+
+
diff --git a/tests/json-handler/multiple-harnesses/config.yml b/tests/json-handler/multiple-harnesses/config.yml
new file mode 100644
index 000000000000..938834ea42cb
--- /dev/null
+++ b/tests/json-handler/multiple-harnesses/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: test.sh
+
diff --git a/tests/json-handler/multiple-harnesses/test.rs b/tests/json-handler/multiple-harnesses/test.rs
new file mode 100644
index 000000000000..f13ac2ae9360
--- /dev/null
+++ b/tests/json-handler/multiple-harnesses/test.rs
@@ -0,0 +1,42 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --export-json multi_harness_output.json
+
+//! Test JSON export with multiple harnesses
+//! Verifies that frontend correctly handles multiple verification harnesses
+
+fn multiply(a: i32, b: i32) -> i32 {
+    a * b
+}
+
+fn divide(a: i32, b: i32) -> i32 {
+    a / b
+}
+
+#[kani::proof]
+fn verify_multiply_positive() {
+    let x: i32 = kani::any();
+    let y: i32 = kani::any();
+    kani::assume(x > 0 && x < 10);
+    kani::assume(y > 0 && y < 10);
+    let result = multiply(x, y);
+    assert!(result > 0);
+}
+
+#[kani::proof]
+fn verify_multiply_zero() {
+    let x: i32 = kani::any();
+    let result = multiply(x, 0);
+    assert_eq!(result, 0);
+}
+
+#[kani::proof]
+fn verify_divide_nonzero() {
+    let x: i32 = kani::any();
+    let y: i32 = kani::any();
+    kani::assume(x >= 0 && x < 100);
+    kani::assume(y > 0 && y < 100);
+    let result = divide(x, y);
+    assert!(result <= x);
+}
diff --git a/tests/json-handler/multiple-harnesses/test.sh b/tests/json-handler/multiple-harnesses/test.sh
new file mode 100755
index 000000000000..b6d5d6a8cd37
--- /dev/null
+++ b/tests/json-handler/multiple-harnesses/test.sh
@@ -0,0 +1,111 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test JSON export with multiple harnesses - validates aggregation logic
+
+set -eu
+# The validator's exit status is piped into `tail` below; without pipefail a failed
+# validation is masked by tail's success and this test passes regardless.
+set -o pipefail
+
+OUTPUT_FILE="multi_harness_output.json"
+# Remove the export on every exit path, not just the happy one: a failing
+# validation step exits early under `set -e` and would otherwise leave it behind.
+trap 'rm -f "$OUTPUT_FILE"' EXIT
+
+# Find the project root
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+VALIDATOR="$PROJECT_ROOT/scripts/validate_json_export.py"
+
+# Run Kani with JSON export
+kani -Z unstable-options test.rs --export-json "$OUTPUT_FILE"
+
+# Check that JSON file was created
+if [ ! -f "$OUTPUT_FILE" ]; then
+    echo "ERROR: JSON file $OUTPUT_FILE was not created"
+    exit 1
+fi
+
+# Validate JSON structure (suppress verbose output)
+python3 "$VALIDATOR" "$OUTPUT_FILE" 2>&1 | tail -1
+
+# Check that the export accounts for all three harnesses: not just that the metadata
+# lists them, but that the summary counters, the per-harness results, and the
+# per-harness detail arrays all agree with each other and with the harnesses that ran.
+python3 << EOF
+import json
+import sys
+
+with open('$OUTPUT_FILE', 'r') as f:
+    data = json.load(f)
+
+expected = {
+    'verify_multiply_positive',
+    'verify_multiply_zero',
+    'verify_divide_nonzero',
+}
+
+failures = []
+
+
+def check(condition, message):
+    if not condition:
+        failures.append(message)
+
+
+metadata_names = {h.get('pretty_name') for h in data['harness_metadata']}
+check(metadata_names == expected,
+      f"harness_metadata should list {sorted(expected)}, got {sorted(map(str, metadata_names))}")
+
+summary = data['verification_results']['summary']
+for field, want in [('total_harnesses', 3), ('executed', 3),
+                    ('successful', 3), ('failed', 0)]:
+    check(summary[field] == want,
+          f"summary.{field} should be {want}, got {summary[field]}")
+
+results = data['verification_results']['results']
+check(len(results) == 3, f"expected 3 results, got {len(results)}")
+result_names = {r.get('harness_id') for r in results}
+check(result_names == expected,
+      f"results should cover {sorted(expected)}, got {sorted(map(str, result_names))}")
+check(all(r.get('status') == 'Success' for r in results),
+      "every harness should report Success")
+
+# Each per-harness array must cover every harness exactly once. These arrays are built
+# in a different order from `results`, so identity has to come from harness_id.
+for key in ['error_details', 'property_details', 'cbmc']:
+    entries = data[key]
+    check(len(entries) == 3, f"expected 3 {key} entries, got {len(entries)}")
+    names = {e.get('harness_id') for e in entries}
+    check(names == expected,
+          f"{key} should cover {sorted(expected)}, got {sorted(map(str, names))}")
+
+check(not any(e.get('has_errors') for e in data['error_details']),
+      "no harness should report errors")
+
+counted = ['passed', 'failed', 'unreachable', 'undetermined', 'solver_error',
+           'satisfied', 'unsatisfiable', 'covered', 'uncovered']
+
+for entry in data['property_details']:
+    details = entry['property_details']
+    harness = entry.get('harness_id')
+    check(details.get('failed') == 0,
+          f"{harness} should have 0 failed properties, got {details.get('failed')}")
+    # The per-status counts must account for every property, or a consumer cannot tell a
+    # complete breakdown from one that quietly dropped a status it did not know about.
+    total = sum(details.get(field) or 0 for field in counted)
+    check(total == details.get('total_properties'),
+          f"{harness} status counts sum to {total} but total_properties is "
+          f"{details.get('total_properties')}")
+
+if failures:
+    for failure in failures:
+        print(f"ERROR: {failure}")
+    sys.exit(1)
+
+print("All three harnesses are accounted for and consistent")
+EOF
+
+
diff --git a/tests/json-handler/schema-validation/config.yml b/tests/json-handler/schema-validation/config.yml
new file mode 100644
index 000000000000..938834ea42cb
--- /dev/null
+++ b/tests/json-handler/schema-validation/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: test.sh
+
diff --git a/tests/json-handler/schema-validation/kani_json_schema.json b/tests/json-handler/schema-validation/kani_json_schema.json
new file mode 100644
index 000000000000..a201f354f1c6
--- /dev/null
+++ b/tests/json-handler/schema-validation/kani_json_schema.json
@@ -0,0 +1,154 @@
+{
+  "_comment": "All fields are required unless listed in _optional. Metadata fields (starting with _) are not validated.",
+  "metadata": {
+    "version": "1.0",
+    "timestamp": "2025-10-30T12:00:00.000000Z",
+    "kani_version": "0.65.0",
+    "target": "x86_64-unknown-linux-gnu",
+    "build_mode": "debug"
+  },
+  "project": {
+    "crate_name": [
+      "example_crate"
+    ],
+    "workspace_root": "/path/to/workspace",
+    "output_dir": "/path/to/workspace/target/x86_64-unknown-linux-gnu/debug/deps"
+  },
+  "tools": {
+    "_optional": [
+      "goto_synthesizer"
+    ],
+    "kani": "0.67.0",
+    "rustc": "rustc 1.95.0-nightly (838709580 2026-02-17)",
+    "cbmc": "6.10.0 (cbmc-6.10.0)",
+    "goto_cc": "clang version 21.0.0 (goto-cc 6.10.0 (cbmc-6.10.0))",
+    "goto_instrument": "6.10.0 (cbmc-6.10.0)",
+    "goto_synthesizer": null,
+    "solvers": [
+      {
+        "name": "cadical",
+        "version": null
+      }
+    ]
+  },
+  "harness_metadata": [
+    {
+      "pretty_name": "example_harness",
+      "mangled_name": "_RNvCs_example_mangled_name",
+      "crate_name": "example_crate",
+      "source": {
+        "file": "src/lib.rs",
+        "start_line": 10,
+        "end_line": 15
+      },
+      "goto_file": "/path/to/goto/file.out",
+      "attributes": {
+        "kind": "Proof",
+        "should_panic": false
+      },
+      "contract": {
+        "contracted_function_name": null,
+        "recursion_tracker": null
+      },
+      "has_loop_contracts": false,
+      "is_automatically_generated": false
+    }
+  ],
+  "verification_results": {
+    "summary": {
+      "total_harnesses": 1,
+      "executed": 1,
+      "status": "completed",
+      "successful": 1,
+      "failed": 0,
+      "duration_ms": 500
+    },
+    "results": [
+      {
+        "harness_id": "example_harness",
+        "status": "Success",
+        "duration_ms": 500,
+        "checks": [
+          {
+            "id": 1,
+            "function": "example_function",
+            "status": "Success",
+            "description": "assertion failed: x > 0",
+            "location": {
+              "file": "src/lib.rs",
+              "line": "20",
+              "column": "13"
+            },
+            "category": "assertion"
+          }
+        ]
+      }
+    ]
+  },
+  "error_details": [
+    {
+      "_optional": [
+        "error_type",
+        "failed_properties_type",
+        "exit_status"
+      ],
+      "harness_id": "example_harness",
+      "has_errors": false,
+      "error_type": null,
+      "failed_properties_type": null,
+      "exit_status": "success"
+    }
+  ],
+  "property_details": [
+    {
+      "harness_id": "example_harness",
+      "property_details": {
+        "_optional": [
+          "error"
+        ],
+        "total_properties": 1,
+        "passed": 1,
+        "failed": 0,
+        "unreachable": 0,
+        "undetermined": 0,
+        "solver_error": 0,
+        "satisfied": 0,
+        "unsatisfiable": 0,
+        "covered": 0,
+        "uncovered": 0,
+        "error": null
+      }
+    }
+  ],
+  "cbmc": [
+    {
+      "_nullable": [
+        "cbmc_stats"
+      ],
+      "harness_id": "example_harness",
+      "cbmc_metadata": {
+        "version": "6.7.1",
+        "os_info": "x86_64 linux unix"
+      },
+      "configuration": {
+        "object_bits": 16,
+        "solver": "Cadical"
+      },
+      "cbmc_stats": {
+        "runtime_symex_s": 0.005,
+        "size_program_expression": 150,
+        "slicing_removed_assignments": 80,
+        "vccs_generated": 1,
+        "vccs_remaining": 1,
+        "runtime_postprocess_equation_s": 2e-05,
+        "runtime_convert_ssa_s": 0.002,
+        "runtime_post_process_s": 5e-06,
+        "runtime_solver_s": 0.0003,
+        "runtime_decision_procedure_s": 0.003
+      }
+    }
+  ],
+  "coverage": {
+    "enabled": false
+  }
+}
diff --git a/tests/json-handler/schema-validation/test.rs b/tests/json-handler/schema-validation/test.rs
new file mode 100644
index 000000000000..df2bea6da730
--- /dev/null
+++ b/tests/json-handler/schema-validation/test.rs
@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --export-json schema_validation_output.json
+
+//! Test JSON schema structure validation
+//! Ensures frontend exports well-formed JSON with correct metadata
+
+fn calculate(x: u32, y: u32) -> u32 {
+    if x > y { x - y } else { y - x }
+}
+
+#[kani::proof]
+fn verify_calculate() {
+    let a: u32 = kani::any();
+    let b: u32 = kani::any();
+    kani::assume(a < 1000);
+    kani::assume(b < 1000);
+    let result = calculate(a, b);
+    assert!(result < 1000);
+}
+
+#[kani::proof]
+fn verify_calculate_same() {
+    let x: u32 = kani::any();
+    let result = calculate(x, x);
+    assert_eq!(result, 0);
+}
diff --git a/tests/json-handler/schema-validation/test.sh b/tests/json-handler/schema-validation/test.sh
new file mode 100755
index 000000000000..0537625a0a59
--- /dev/null
+++ b/tests/json-handler/schema-validation/test.sh
@@ -0,0 +1,78 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test JSON schema structure from schema_utils.rs functions
+# This test uses the schema template to validate the JSON output
+
+set -eu
+
+OUTPUT_FILE="schema_output.json"
+# Remove the export on every exit path, not just the happy one: a failing
+# validation step exits early under `set -e` and would otherwise leave it behind.
+trap 'rm -f "$OUTPUT_FILE"' EXIT
+
+# Find the project root (where scripts/ directory is)
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+VALIDATOR="$PROJECT_ROOT/scripts/validate_json_export.py"
+
+# Run Kani with JSON export
+kani -Z unstable-options test.rs --export-json "$OUTPUT_FILE"
+
+# Check that JSON file was created
+if [ ! -f "$OUTPUT_FILE" ]; then
+    echo "ERROR: JSON file $OUTPUT_FILE was not created"
+    exit 1
+fi
+
+echo "JSON file created"
+
+# Validate basic structure using schema template
+python3 "$VALIDATOR" "$OUTPUT_FILE"
+
+# Validate each field from schema template dynamically
+echo ""
+echo "Validating individual fields from schema:"
+
+# Get all top-level keys from schema and validate each that exists in JSON
+SCHEMA_FILE="$(dirname "$0")/kani_json_schema.json"
+python3 << EOF
+import json
+import subprocess
+import sys
+
+with open('$SCHEMA_FILE', 'r') as f:
+    schema = json.load(f)
+
+with open('$OUTPUT_FILE', 'r') as f:
+    data = json.load(f)
+
+all_passed = True
+for key in schema.keys():
+    if key not in data:
+        continue
+    
+    result = subprocess.run(
+        ['python3', '$VALIDATOR', '$OUTPUT_FILE', '--field-path', key],
+        capture_output=True
+    )
+    if result.returncode == 0:
+        print(f"  {key}: PASSED")
+    else:
+        print(f"  {key}: FAILED")
+        all_passed = False
+
+if not all_passed:
+    sys.exit(1)
+EOF
+
+if [ $? -ne 0 ]; then
+    echo "Field validation failed"
+    exit 1
+fi
+
+
+echo ""
+echo "All validations passed"
+