From e78ac29fdfb0521de9c58b811dd8eec0bcf5e612 Mon Sep 17 00:00:00 2001
From: Ivo Matijasevic <ivomatijasevic@gmail.com>
Date: Wed, 12 Aug 2026 23:39:27 +0200
Subject: [PATCH 1/5] export-json: don't report failed, skipped, or zero-match
 runs as complete

Close several ways a run that did not finish cleanly could still serialize as a clean, completed export:

- A run reusing an --export-json path that died before the final write (compile error, OOM, Ctrl-C, or a
  harness-level error propagating out) left the *previous* run's complete-looking file at the target.
  verify_project now writes a run_state:"incomplete" marker to the target before verification starts, so a
  stale file can never be read as this run's result; the marker is promoted to "complete" only when the
  run finished.
- A --harness filter that matched nothing wrote a completed / 0-failed document (the "no harnesses
  matched" error is only raised after the export). A zero-match run is now marked
  run_state:"no_harnesses_selected", and a harness_selection block records the requested filters, the
  matched count, and any unmatched filters.
- Under --fail-fast, harnesses skipped after the first failure kept their harness_metadata entry but had
  no error_details/property_details entry, so a consumer correlating the arrays could read absence as
  success. Every selected harness now gets an explicit entry, and the terminal run_state is "complete"
  only when every selected harness produced a result, "partial" otherwise.
- Per-harness details were joined to results on pretty_name, which two harnesses in different crates of a
  workspace can share, misattributing a result. The join now uses the unique mangled_name.

Follow-up to #4472.
---
 kani-driver/src/frontend/schema_utils.rs | 60 ++++++++++++++++++++--
 kani-driver/src/main.rs                  | 63 ++++++++++++++++++++++++
 2 files changed, 118 insertions(+), 5 deletions(-)

diff --git a/kani-driver/src/frontend/schema_utils.rs b/kani-driver/src/frontend/schema_utils.rs
index 2984f640b00..88bbfb1fd9e 100644
--- a/kani-driver/src/frontend/schema_utils.rs
+++ b/kani-driver/src/frontend/schema_utils.rs
@@ -177,8 +177,9 @@ impl PropertyCounts {
         })
     }
 
-    /// The same shape, for a harness whose properties were never measured.
-    fn unmeasured_json() -> Value {
+    /// The same shape, for a harness whose properties were never measured, with a caller-supplied
+    /// explanation of why (e.g. a CBMC failure vs. never having run at all).
+    fn unmeasured_json_with_reason(reason: &str) -> Value {
         json!({
             "total_properties": null,
             "passed": null,
@@ -190,9 +191,16 @@ impl PropertyCounts {
             "unsatisfiable": null,
             "covered": null,
             "uncovered": null,
-            "error": "Could not extract property details due to verification failure"
+            "error": reason
         })
     }
+
+    /// The same shape, for a harness whose properties were never measured.
+    fn unmeasured_json() -> Value {
+        Self::unmeasured_json_with_reason(
+            "Could not extract property details due to verification failure",
+        )
+    }
 }
 
 /// Creates structured JSON metadata for the project
@@ -326,7 +334,12 @@ pub fn process_harness_results(
 ) -> 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);
+        // Joined on `mangled_name`, the unique identifier `harness_metadata` already carries,
+        // rather than `pretty_name`: two harnesses in different crates of the same workspace can
+        // share a `pretty_name`, and joining on that would attribute a result -- including a
+        // failure -- to the wrong harness. `harness_id` in the emitted JSON is unchanged; only
+        // the join predicate used to find the matching result moves to the unique key.
+        let harness_result = results.iter().find(|r| r.harness.mangled_name == h.mangled_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
@@ -377,6 +390,40 @@ pub fn process_harness_results(
                     }
                 }),
             );
+        } else {
+            // This harness was selected (it has a `harness_metadata` entry) but has no entry in
+            // `results`. That is not always "never ran": under `--fail-fast`,
+            // `check_all_harnesses` collects harness futures into a single `Result<Vec<_>>`, and
+            // as soon as one harness fails, the whole collection short-circuits on that `Err` --
+            // discarding the `Ok` results of any other harness that had already completed
+            // (including a pass) but lost the race to be collected before the failure. So a
+            // harness landing in this branch may have genuinely been skipped, or may have run
+            // and even passed, with its result simply not retained. Without this branch the
+            // harness would be silently absent from both `error_details` and `property_details`,
+            // which a consumer correlating those arrays against `harness_metadata` (or checking
+            // "every detail entry is a Success") could easily misread as "nothing wrong with it".
+            // "skipped"/"not_run" would overclaim the former case for certain, so this reports
+            // the honest, disjunctive truth instead.
+            handler.add_harness_detail(
+                "error_details",
+                json!({
+                    "harness_id": h.pretty_name,
+                    "has_errors": true,
+                    "error_type": "not_reported",
+                    "exit_status": "unknown"
+                }),
+            );
+
+            handler.add_harness_detail(
+                "property_details",
+                json!({
+                    "harness_id": h.pretty_name,
+                    "property_details": PropertyCounts::unmeasured_json_with_reason(
+                        "No result was reported for this harness (e.g. skipped after \
+                         --fail-fast, or a completed result not retained)."
+                    )
+                }),
+            );
         }
     }
 
@@ -468,7 +515,10 @@ pub fn process_cbmc_results(
 ) -> 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);
+        // See the matching comment in `process_harness_results`: join on the unique
+        // `mangled_name` rather than `pretty_name`, which two harnesses in different crates of a
+        // workspace can share.
+        let harness_result = results.iter().find(|r| r.harness.mangled_name == h.mangled_name);
         handler.add_harness_detail("cbmc", json!({
             // basic name for harnesses
             "harness_id": h.pretty_name,
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 22aad350eb4..1754b5602a8 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -147,6 +147,23 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
     // 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())));
+
+    // Invalidate any stale export at the target path immediately, before verification even
+    // starts. Without this, a run that dies before reaching the final `export()` below (a
+    // compile error, OOM, Ctrl-C, or a harness-level `Err` that propagates out of this function
+    // before that export runs) would leave a *previous* run's clean, complete-looking file at
+    // the target path -- and a consumer that trusts the file would read it as this run's
+    // result. Writing this marker first means the target can never be read as a stale clean pass
+    // again: it is either this incomplete marker, a genuinely complete export from this run, or
+    // absent. `write_sarif`/`print_final_summary` below run *after* the final `export()`, using
+    // the same `results` the export was built from, so a failure there leaves behind a complete
+    // export whose verification data is already accurate -- it is not a case this marker needs
+    // to guard against.
+    if let Some(handler) = handler.as_mut() {
+        handler.add_item("run_state", json!("incomplete"));
+        handler.export()?;
+    }
+
     let harnesses = session.determine_targets(project.get_all_harnesses())?;
     debug!(n = harnesses.len(), ?harnesses, "verify_project");
 
@@ -168,6 +185,41 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
         for h in &harnesses {
             handler.add_harness_detail("harness_metadata", create_harness_metadata_json(h));
         }
+
+        // Record what was requested and what was actually selected, so a filter typo that
+        // matches nothing is visible in the export itself rather than only in a log line the
+        // export's consumer never sees.
+        let requested_filters = &session.args.harnesses;
+        let unmatched_filters: Vec<&String> = if session.args.exact {
+            // `determine_targets` above already returns an error when an `--exact` filter
+            // matches nothing, so reaching this point means every exact filter matched.
+            vec![]
+        } else {
+            // Mirrors `find_proof_harnesses`'s non-exact matching closely enough to be a useful
+            // diagnostic (exact and unqualified-name matches are also substring matches of the
+            // full pretty name), without needing to re-run its full matching logic here.
+            requested_filters
+                .iter()
+                .filter(|filter| !harnesses.iter().any(|h| h.pretty_name.contains(filter.as_str())))
+                .collect()
+        };
+        handler.add_item(
+            "harness_selection",
+            json!({
+                "requested_filters": requested_filters,
+                "matched_count": harnesses.len(),
+                "unmatched_filters": unmatched_filters,
+            }),
+        );
+
+        if harnesses.is_empty() {
+            // A filter that matches zero harnesses must never export as a clean, completed run
+            // with `successful:0, failed:0` -- that is a vacuous pass, not evidence of anything.
+            // This overrides the "incomplete" marker written above; the final block below only
+            // promotes a run to "complete" when at least one harness was actually selected, so
+            // this state survives to the exported file.
+            handler.add_item("run_state", json!("no_harnesses_selected"));
+        }
     }
 
     // Verification
@@ -201,6 +253,17 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
 
     if let Some(handler) = handler.as_mut() {
         handler.add_item("coverage", json!({"enabled": session.args.coverage}));
+        // The terminal `run_state` must be authoritative about whether every selected harness
+        // actually ran: a zero-match run keeps the `no_harnesses_selected` state set above, and
+        // -- critically -- a non-empty selection is only "complete" when `results` accounts for
+        // every selected harness. Under `--fail-fast`, harnesses skipped after the first failure
+        // never produce a `HarnessResult`, so `results.len() < harnesses.len()`; reporting
+        // "complete" in that case would say a run that was intentionally aborted early finished
+        // normally. That case is reported as "partial" instead.
+        if !harnesses.is_empty() {
+            let run_state = if results.len() == harnesses.len() { "complete" } else { "partial" };
+            handler.add_item("run_state", json!(run_state));
+        }
         handler.export()?;
     }
 

From e17eff28432374c0aeb9fcce3b4c6020ca545d1c Mon Sep 17 00:00:00 2001
From: Ivo Matijasevic <ivomatijasevic@gmail.com>
Date: Wed, 12 Aug 2026 23:39:27 +0200
Subject: [PATCH 2/5] export-json: cbmc_stats parsing is non-destructive,
 unit-safe, and overflow-safe

The scraped CBMC statistics could be silently wrong:

- A later status message that matched a recognized label but failed to parse overwrote an
  already-recorded valid value with null (indistinguishable from "not measured"). Parsing now only
  assigns on success and never clobbers a valid value.
- Exact-suffix matching turned any harmless CBMC wording change into a silent null. Counts now parse the
  leading numeric token, tolerating trailing text.
- record_seconds extracted the leading number regardless of unit, so a duration reported as "5ms" would
  be recorded as 5 seconds. It now accepts a value only when the unit is exactly "s"; any other unit is a
  parse failure, never a mis-scaled number.
- The integer count fields were u32; a large enough run overflowed to null. Widened to u64.

Follow-up to #4472.
---
 kani-driver/src/call_cbmc.rs | 135 +++++++++++++++++++++++++++++++----
 1 file changed, 121 insertions(+), 14 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index dc4ae72b2db..d1cc218c3f2 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -37,10 +37,14 @@ pub struct CbmcInfo {
 #[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>,
+    // `u64`, not `u32`: these are unbounded counts scraped from CBMC's own text output (program
+    // expression size, VCCs, sliced assignments), and a sufficiently large real run overflowing
+    // `u32` used to collapse silently to `null` via `parse::<u32>().ok()` -- indistinguishable
+    // from "not measured".
+    pub size_program_expression: Option<u64>,
+    pub slicing_removed_assignments: Option<u64>,
+    pub vccs_generated: Option<u64>,
+    pub vccs_remaining: Option<u64>,
     pub runtime_postprocess_equation_s: Option<f64>,
     pub runtime_convert_ssa_s: Option<f64>,
     pub runtime_post_process_s: Option<f64>,
@@ -107,6 +111,12 @@ fn merge_cbmc_stats(items: &[ParserItem]) -> Option<CbmcStats> {
 /// 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.
+///
+/// Every field assignment below goes through [`record_stat`], which only overwrites a field when
+/// parsing succeeds. Without that, a later message that merely *resembles* a recognized label but
+/// fails to parse (a wording tweak, an unexpected unit, a truncated line) would silently erase an
+/// already-recorded valid measurement by assigning it `None` -- indistinguishable from "never
+/// measured" to a consumer of the export.
 fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
     // "Generated 1 VCC(s), 1 remaining after simplification"
     if let Some(counts) = message
@@ -114,9 +124,9 @@ fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
         .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();
+        let generated_ok = record_stat(&mut stats.vccs_generated, parse_leading_number(generated));
+        let remaining_ok = record_stat(&mut stats.vccs_remaining, parse_leading_number(remaining));
+        return generated_ok || remaining_ok;
     }
 
     // "slicing removed 81 assignments", or "simple slicing removed 5 assignments" when only the
@@ -126,8 +136,7 @@ fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
             .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();
+        return record_stat(&mut stats.slicing_removed_assignments, parse_leading_number(count));
     }
 
     // Everything else is reported as "<label>: <value>".
@@ -137,9 +146,7 @@ fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
     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()
+            record_stat(&mut stats.size_program_expression, parse_leading_number(value))
         }
         "Runtime Symex" => record_seconds(value, &mut stats.runtime_symex_s),
         "Runtime Postprocess Equation" => {
@@ -155,10 +162,60 @@ fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
     }
 }
 
+/// Assign a freshly parsed value to `field` only when parsing succeeded. Never clobbers a
+/// previously recorded valid value with `None` -- a `parse` failure simply leaves whatever `field`
+/// already held. Returns whether this update recognized a value.
+fn record_stat<T>(field: &mut Option<T>, parsed: Option<T>) -> bool {
+    match parsed {
+        Some(value) => {
+            *field = Some(value);
+            true
+        }
+        None => false,
+    }
+}
+
+/// Parse the leading numeric token of `s` (optionally signed, with an optional decimal point and
+/// exponent), together with whatever non-numeric text remains afterwards, trimmed. A caller that
+/// does not care about the trailing text (a count, where the label alone already disambiguates
+/// the unit) can use [`parse_leading_number`]; a caller for which the unit is meaningful -- see
+/// [`record_seconds`] -- can inspect the remainder before trusting the value.
+fn parse_leading_number_with_remainder<T: std::str::FromStr>(s: &str) -> Option<(T, &str)> {
+    let s = s.trim();
+    let end = s
+        .find(|c: char| !(c.is_ascii_digit() || matches!(c, '.' | '-' | '+' | 'e' | 'E')))
+        .unwrap_or(s.len());
+    if end == 0 {
+        return None;
+    }
+    let value = s[..end].parse().ok()?;
+    Some((value, s[end..].trim()))
+}
+
+/// Parse the leading numeric token of `s`, ignoring anything that follows -- a trailing unit like
+/// `" steps"`, or any other suffix. This is more robust than matching an exact suffix: a harmless
+/// CBMC wording change to the text *after* the number (a new unit, a pluralization change, extra
+/// trailing detail) still lets the number itself be recovered, rather than silently collapsing
+/// the whole measurement to `null`. Only use this where the unit doesn't affect the *meaning* of
+/// the number -- for durations, see [`record_seconds`], which does check the unit.
+fn parse_leading_number<T: std::str::FromStr>(s: &str) -> Option<T> {
+    parse_leading_number_with_remainder(s).map(|(value, _)| value)
+}
+
 /// Record a duration CBMC reports as "0.00408627s" or "1.5416e-05s".
+///
+/// Unlike the count fields (see [`parse_leading_number`]), the unit here is meaningful: a value
+/// CBMC reported in another unit -- "5ms", say -- would have its leading number "5" extracted
+/// just as readily as "5s", but recording it as 5 *seconds* would silently misreport it by three
+/// orders of magnitude. So the value is only accepted when the text remaining after the leading
+/// number is exactly "s"; any other unit, or any other trailing text, is treated as a parse
+/// failure -- never as a number recorded in the wrong scale. See [`record_stat`] for why a parse
+/// failure never clobbers a previously recorded valid value.
 fn record_seconds(value: &str, field: &mut Option<f64>) -> bool {
-    *field = value.strip_suffix('s').and_then(|seconds| seconds.parse().ok());
-    field.is_some()
+    let parsed = parse_leading_number_with_remainder::<f64>(value)
+        .filter(|(_, remainder)| *remainder == "s")
+        .map(|(seconds, _)| seconds);
+    record_stat(field, parsed)
 }
 
 /// We will use Cadical by default since it performed better than MiniSAT in our analysis.
@@ -787,6 +844,56 @@ mod tests {
         assert!(merge_cbmc_stats(&warning).is_none());
     }
 
+    /// A later message that fails to parse must never erase an already-recorded valid value: the
+    /// gap between "not measured" and "we saw a value we couldn't parse" must stay visible as
+    /// "we kept the value we did successfully parse", not collapse to `null`.
+    #[test]
+    fn check_cbmc_stats_never_clobbers_valid_value() {
+        let mut stats = CbmcStats::default();
+        assert!(record_cbmc_stat("Runtime Solver: 4.1167e-05s", &mut stats));
+        assert_eq!(stats.runtime_solver_s, Some(4.1167e-05));
+
+        // A later malformed duplicate of the same label must not erase the value already
+        // recorded above.
+        assert!(!record_cbmc_stat("Runtime Solver: not-a-number", &mut stats));
+        assert_eq!(stats.runtime_solver_s, Some(4.1167e-05));
+    }
+
+    /// Parsing the leading numeric token (rather than requiring an exact suffix match) tolerates
+    /// harmless trailing text a suffix-based parser would reject outright.
+    #[test]
+    fn check_cbmc_stats_leading_number_tolerates_trailing_text() {
+        let mut stats = CbmcStats::default();
+        assert!(record_cbmc_stat(
+            "size of program expression: 21 steps (post-slicing)",
+            &mut stats
+        ));
+        assert_eq!(stats.size_program_expression, Some(21));
+    }
+
+    /// `record_seconds` must not mistake a value reported in another unit for seconds: the
+    /// leading number "5" is just as extractable from "5ms" as from "5s", but recording it as 5
+    /// seconds would misreport it by three orders of magnitude. Only an exact "s" suffix is
+    /// accepted; genuine second values, including exponent notation, still parse.
+    #[test]
+    fn check_record_seconds_is_unit_safe() {
+        let mut none = None;
+        assert!(!record_seconds("5ms", &mut none));
+        assert_eq!(none, None);
+
+        let mut none = None;
+        assert!(!record_seconds("5", &mut none));
+        assert_eq!(none, None);
+
+        let mut seconds = None;
+        assert!(record_seconds("0.004s", &mut seconds));
+        assert_eq!(seconds, Some(0.004));
+
+        let mut seconds = None;
+        assert!(record_seconds("1.5e-05s", &mut seconds));
+        assert_eq!(seconds, Some(1.5e-05));
+    }
+
     /// No statistics at all (CBMC died early, or verbosity hid them) must not fabricate a record.
     #[test]
     fn check_cbmc_stats_absent() {

From 1b06440d32dfb426f925bd6f58967a4a674675cc Mon Sep 17 00:00:00 2001
From: Ivo Matijasevic <ivomatijasevic@gmail.com>
Date: Wed, 12 Aug 2026 23:39:27 +0200
Subject: [PATCH 3/5] export-json: validator checks leaf types, count
 semantics, and run_state

The shipped validator checked structure but not values or semantics, so a structurally well-formed
document that misreported -- failed:-1, successful:"yes", executed disagreeing with results, or
run_state:"complete" with empty results -- validated as OK. It now checks leaf value types, non-negative
and reconciled summary counts, and the run_state enum and its invariants, with a validator-negative test
suite covering each. run_state and harness_selection are added to the schema template so their presence
is required.

Follow-up to #4472.
---
 scripts/validate_json_export.py               | 127 +++++++++++++++++-
 .../schema-validation/kani_json_schema.json   |  10 +-
 .../validator-negative/build_fixtures.py      |  76 +++++++++++
 .../validator-negative/config.yml             |   3 +
 tests/json-handler/validator-negative/test.sh |  61 +++++++++
 5 files changed, 273 insertions(+), 4 deletions(-)
 create mode 100755 tests/json-handler/validator-negative/build_fixtures.py
 create mode 100644 tests/json-handler/validator-negative/config.yml
 create mode 100755 tests/json-handler/validator-negative/test.sh

diff --git a/scripts/validate_json_export.py b/scripts/validate_json_export.py
index 22cba5a8745..ff74a3948fb 100755
--- a/scripts/validate_json_export.py
+++ b/scripts/validate_json_export.py
@@ -100,18 +100,135 @@ def validate_structure_recursive(data, schema, path="", nullable=False):
             # 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.
+            #
+            # An empty array is *not* treated as an error here: some arrays are legitimately
+            # empty (e.g. `checks` for a harness with no properties). What used to make an empty
+            # array a vacuous pass was that it skips the loop below with zero iterations and
+            # zero errors -- exactly like a real, correctly-validated array. The distinction
+            # this function draws is between "validated everything present" (this) and
+            # "nothing was present to check" (a caller-level semantic question, e.g. whether
+            # `results` should be empty -- see `validate_semantic_checks`).
             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
+    # Leaf values. A `None` schema leaf means the template does not commit to a type at this
+    # position (e.g. `contract.contracted_function_name`, which is only ever populated from real
+    # data) -- there's nothing to check against, so it is left unvalidated exactly as before.
+    # A non-`None` schema leaf, on the other hand, is a definite type (bool / number / string),
+    # and the data must match it. Before this, `"failed": -100`, `"successful": "yes"`, or any
+    # other leaf of the wrong type validated as OK, because leaves were never inspected at all.
+    elif schema is not None:
+        if isinstance(schema, bool):
+            # Must come before the `int`/`float` branch: in Python, `bool` is a subclass of
+            # `int`, so `isinstance(True, int)` is true and would otherwise let a bool through
+            # a numeric check (and vice versa below).
+            if not isinstance(data, bool):
+                errors.append(
+                    f"Type mismatch at {path}: expected bool, got {type(data).__name__}"
+                )
+        elif isinstance(schema, (int, float)):
+            if isinstance(data, bool) or not isinstance(data, (int, float)):
+                errors.append(
+                    f"Type mismatch at {path}: expected a number, got {type(data).__name__}"
+                )
+        elif isinstance(schema, str):
+            if not isinstance(data, str):
+                errors.append(
+                    f"Type mismatch at {path}: expected str, got {type(data).__name__}"
+                )
 
     success = len(errors) == 0
     return success, errors
 
 
+def validate_semantic_checks(data):
+    """
+    A small set of semantic checks on `verification_results.summary` beyond structure and leaf
+    types: a document can be perfectly well-typed and still lie about what happened, e.g.
+    `executed` disagreeing with the number of results actually reported, or a negative count that
+    is well-typed (a valid JSON integer) but meaningless. Kept deliberately narrow -- this is not
+    a general semantic validator, just the reconciliation checks a mutated count can defeat.
+
+    Returns a list of error strings; an empty list means the semantic checks found nothing wrong.
+    """
+    errors = []
+
+    verification_results = data.get("verification_results")
+    if not isinstance(verification_results, dict):
+        # Already reported (or not applicable) by the structural check; nothing more to say here.
+        return errors
+
+    summary = verification_results.get("summary")
+    results = verification_results.get("results")
+    if not isinstance(summary, dict) or not isinstance(results, list):
+        return errors
+
+    def as_int(value):
+        # Excludes `bool`: a `True`/`False` count is a type error the structural check already
+        # reports, not a value this function should reason about numerically.
+        return value if isinstance(value, int) and not isinstance(value, bool) else None
+
+    executed = as_int(summary.get("executed"))
+    successful = as_int(summary.get("successful"))
+    failed = as_int(summary.get("failed"))
+
+    for field in ("total_harnesses", "executed", "successful", "failed", "duration_ms"):
+        value = as_int(summary.get(field))
+        if value is not None and value < 0:
+            errors.append(
+                f"verification_results.summary.{field} is negative: {value}"
+            )
+
+    if executed is not None and executed != len(results):
+        errors.append(
+            f"verification_results.summary.executed ({executed}) does not match "
+            f"the number of entries in verification_results.results ({len(results)})"
+        )
+
+    if executed is not None and successful is not None and failed is not None:
+        if successful + failed != executed:
+            errors.append(
+                f"verification_results.summary.successful ({successful}) + "
+                f"failed ({failed}) does not equal executed ({executed})"
+            )
+
+    # `run_state` is the field a consumer is meant to trust as the run's bottom line, so its
+    # value must both be one of the states the exporter actually emits, and must agree with what
+    # the rest of the document says happened -- otherwise a mislabeled `run_state` is a more
+    # dangerous lie than no `run_state` at all.
+    run_state = data.get("run_state")
+    if run_state is not None:
+        valid_run_states = {"incomplete", "no_harnesses_selected", "partial", "complete"}
+        if run_state not in valid_run_states:
+            errors.append(
+                f"run_state has an unrecognized value: {run_state!r} "
+                f"(expected one of {sorted(valid_run_states)})"
+            )
+        elif run_state == "complete":
+            if len(results) == 0:
+                errors.append(
+                    'run_state is "complete" but verification_results.results is empty'
+                )
+            # `executed == len(results)` is already enforced unconditionally above, so a
+            # "complete" run that disagrees is already reported there.
+        elif run_state == "no_harnesses_selected":
+            if executed is not None and executed != 0:
+                errors.append(
+                    'run_state is "no_harnesses_selected" but '
+                    f"verification_results.summary.executed is {executed}, expected 0"
+                )
+            if len(results) != 0:
+                errors.append(
+                    'run_state is "no_harnesses_selected" but '
+                    f"verification_results.results is not empty (len={len(results)})"
+                )
+
+    return errors
+
+
 def validate_json_structure(json_file, schema=None):
     """
     Validate that JSON export matches the schema template structure.
@@ -134,9 +251,13 @@ def validate_json_structure(json_file, schema=None):
 
     # 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, "")
+    _, structural_errors = validate_structure_recursive(data, schema, "")
+
+    # Structural/type validation and semantic validation are independent: run both and report
+    # everything found, rather than short-circuiting on the first kind of failure.
+    all_errors = structural_errors + validate_semantic_checks(data)
 
-    if not success or all_errors:
+    if all_errors:
         print(f"ERROR: Validation failed for {json_file}:")
         for error in all_errors:
             print(f"  - {error}")
diff --git a/tests/json-handler/schema-validation/kani_json_schema.json b/tests/json-handler/schema-validation/kani_json_schema.json
index a201f354f1c..5a9ede4d9cc 100644
--- a/tests/json-handler/schema-validation/kani_json_schema.json
+++ b/tests/json-handler/schema-validation/kani_json_schema.json
@@ -54,6 +54,13 @@
       "is_automatically_generated": false
     }
   ],
+  "harness_selection": {
+    "requested_filters": [
+      "example_harness"
+    ],
+    "matched_count": 1,
+    "unmatched_filters": []
+  },
   "verification_results": {
     "summary": {
       "total_harnesses": 1,
@@ -150,5 +157,6 @@
   ],
   "coverage": {
     "enabled": false
-  }
+  },
+  "run_state": "complete"
 }
diff --git a/tests/json-handler/validator-negative/build_fixtures.py b/tests/json-handler/validator-negative/build_fixtures.py
new file mode 100755
index 00000000000..f6363638be5
--- /dev/null
+++ b/tests/json-handler/validator-negative/build_fixtures.py
@@ -0,0 +1,76 @@
+#!/usr/bin/env python3
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+"""
+Builds fixture JSON documents for `scripts/validate_json_export.py`'s negative tests.
+
+Starting point is the schema template itself, with its schema-only metadata keys
+(`_comment`, `_optional`, `_nullable`) stripped out recursively: what remains is a document
+built entirely from the template's own values, which validates cleanly against the template
+(each fixture's "valid" baseline). Each malformed fixture then applies one targeted mutation --
+each mutation is a case the old, leaf-type-blind validator accepted vacuously.
+"""
+
+import copy
+import json
+import sys
+
+
+def strip_meta(node):
+    if isinstance(node, dict):
+        return {k: strip_meta(v) for k, v in node.items() if not k.startswith("_")}
+    if isinstance(node, list):
+        return [strip_meta(item) for item in node]
+    return node
+
+
+def write(out_dir, name, doc):
+    with open(f"{out_dir}/{name}", "w") as f:
+        json.dump(doc, f, indent=2)
+
+
+def main():
+    if len(sys.argv) != 3:
+        print("usage: build_fixtures.py <schema_template.json> <output_dir>")
+        sys.exit(1)
+    schema_path, out_dir = sys.argv[1], sys.argv[2]
+
+    with open(schema_path) as f:
+        schema = json.load(f)
+
+    valid = strip_meta(schema)
+    write(out_dir, "valid_export.json", valid)
+
+    # A negative count: well-typed (a real JSON integer), but meaningless. The
+    # `"failed": -100`-style mutation from the issue report.
+    negative_count = copy.deepcopy(valid)
+    negative_count["verification_results"]["summary"]["failed"] = -1
+    write(out_dir, "malformed_negative_count.json", negative_count)
+
+    # A count reported as the wrong JSON type entirely.
+    wrong_type = copy.deepcopy(valid)
+    wrong_type["verification_results"]["summary"]["successful"] = "yes"
+    write(out_dir, "malformed_wrong_type.json", wrong_type)
+
+    # `executed` disagreeing with the actual number of entries in `results` -- well-typed and
+    # individually non-negative, only wrong once the two are reconciled against each other.
+    count_mismatch = copy.deepcopy(valid)
+    count_mismatch["verification_results"]["summary"]["executed"] = 99
+    write(out_dir, "malformed_count_mismatch.json", count_mismatch)
+
+    # `run_state: "complete"` claiming a clean finish while `results` is empty -- exactly the
+    # shape a zero-match or killed-before-verifying run must never be mistaken for. The rest of
+    # the summary is kept internally consistent (0 executed, 0 successful/failed) so this fixture
+    # isolates the `run_state == "complete"` invariant specifically.
+    complete_with_empty_results = copy.deepcopy(valid)
+    complete_with_empty_results["run_state"] = "complete"
+    complete_with_empty_results["verification_results"]["results"] = []
+    summary = complete_with_empty_results["verification_results"]["summary"]
+    summary["executed"] = 0
+    summary["successful"] = 0
+    summary["failed"] = 0
+    write(out_dir, "malformed_complete_with_empty_results.json", complete_with_empty_results)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/tests/json-handler/validator-negative/config.yml b/tests/json-handler/validator-negative/config.yml
new file mode 100644
index 00000000000..8258439d3e3
--- /dev/null
+++ b/tests/json-handler/validator-negative/config.yml
@@ -0,0 +1,3 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: test.sh
diff --git a/tests/json-handler/validator-negative/test.sh b/tests/json-handler/validator-negative/test.sh
new file mode 100755
index 00000000000..6b059e59024
--- /dev/null
+++ b/tests/json-handler/validator-negative/test.sh
@@ -0,0 +1,61 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Negative test for `scripts/validate_json_export.py` itself, not for `--export-json`'s output.
+# It does not invoke Kani or CBMC at all: it only exercises the validator against synthetic
+# fixtures built from the schema template.
+#
+# Before the validator hardening (targeting #4472's follow-up), `validate_structure_recursive`
+# checked keys and nesting but never leaf value types, and count semantics were never checked at
+# all. That let a document like `"failed": -100` or `"successful": "yes"` validate as OK, giving
+# false CI confidence to anyone using this validator as a pass/fail oracle. This test asserts the
+# opposite is now true: a document that is structurally well-formed but carries a corrupted value
+# is REJECTED (non-zero exit).
+
+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"
+SCHEMA="$PROJECT_ROOT/tests/json-handler/schema-validation/kani_json_schema.json"
+
+WORK_DIR="$(mktemp -d)"
+trap 'rm -rf "$WORK_DIR"' EXIT
+
+python3 "$SCRIPT_DIR/build_fixtures.py" "$SCHEMA" "$WORK_DIR"
+
+echo "Checking a well-formed export still validates..."
+python3 "$VALIDATOR" "$WORK_DIR/valid_export.json"
+
+echo ""
+echo "Checking a malformed export (verification_results.summary.failed: -1) is now rejected..."
+if python3 "$VALIDATOR" "$WORK_DIR/malformed_negative_count.json"; then
+    echo "ERROR: validator accepted a document with a negative 'failed' count"
+    exit 1
+fi
+
+echo ""
+echo "Checking a malformed export (verification_results.summary.successful: \"yes\") is now rejected..."
+if python3 "$VALIDATOR" "$WORK_DIR/malformed_wrong_type.json"; then
+    echo "ERROR: validator accepted a document with successful:\"yes\" (a string, not a number)"
+    exit 1
+fi
+
+echo ""
+echo "Checking a malformed export (summary.executed disagreeing with len(results)) is now rejected..."
+if python3 "$VALIDATOR" "$WORK_DIR/malformed_count_mismatch.json"; then
+    echo "ERROR: validator accepted a document where summary.executed disagreed with len(results)"
+    exit 1
+fi
+
+echo ""
+echo "Checking a malformed export (run_state: \"complete\" with results: []) is now rejected..."
+if python3 "$VALIDATOR" "$WORK_DIR/malformed_complete_with_empty_results.json"; then
+    echo "ERROR: validator accepted run_state:\"complete\" with an empty results array"
+    exit 1
+fi
+
+echo ""
+echo "All validator negative-test checks passed"

From de4312e4d76b12b4ec0a108bec19e75710689d8c Mon Sep 17 00:00:00 2001
From: Ivo Matijasevic <ivomatijasevic@gmail.com>
Date: Thu, 13 Aug 2026 00:56:00 +0200
Subject: [PATCH 4/5] Allow a null workspace_root in the export-json schema
 validator

A standalone (non-Cargo) run has no workspace root, so `project.workspace_root`
is legitimately null. The strengthened leaf-type validation rejected that null
as a type mismatch against the string in the schema template, failing the
json-handler exec tests on every standalone harness. Mark the field _nullable so
a null is accepted while a wrong non-null type is still rejected.
---
 tests/json-handler/schema-validation/kani_json_schema.json | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tests/json-handler/schema-validation/kani_json_schema.json b/tests/json-handler/schema-validation/kani_json_schema.json
index 5a9ede4d9cc..6bbb1db2d64 100644
--- a/tests/json-handler/schema-validation/kani_json_schema.json
+++ b/tests/json-handler/schema-validation/kani_json_schema.json
@@ -8,6 +8,9 @@
     "build_mode": "debug"
   },
   "project": {
+    "_nullable": [
+      "workspace_root"
+    ],
     "crate_name": [
       "example_crate"
     ],

From e6633c5338e1a0c5f261d8dd4367c8092cd4a04d Mon Sep 17 00:00:00 2001
From: Ivo Matijasevic <ivomatijasevic@gmail.com>
Date: Thu, 13 Aug 2026 17:51:00 +0200
Subject: [PATCH 5/5] Accept legitimately-null leaves in the export-json
 validator

The strengthened leaf-type validation rejected the nulls that --export-json
emits on ordinary degraded runs: unmeasured per-harness property counts (a
timed-out or OOM'd harness reports them as null, not zero, so a degraded run
is not mistaken for "nothing failed"), partial cbmc_stats, an --smt2 run that
names no solver, and unavailable tool/CBMC versions. Mark those leaves
_nullable in the schema template so a null is accepted while a wrong non-null
type is still rejected, and extend the validator test with degraded-run
fixtures (and a null-in-a-required-field fixture that must still be rejected).
---
 .../schema-validation/kani_json_schema.json   | 39 ++++++++++++
 .../validator-negative/build_fixtures.py      | 59 +++++++++++++++++++
 tests/json-handler/validator-negative/test.sh | 23 ++++++++
 3 files changed, 121 insertions(+)

diff --git a/tests/json-handler/schema-validation/kani_json_schema.json b/tests/json-handler/schema-validation/kani_json_schema.json
index 6bbb1db2d64..207dfe30d5b 100644
--- a/tests/json-handler/schema-validation/kani_json_schema.json
+++ b/tests/json-handler/schema-validation/kani_json_schema.json
@@ -21,6 +21,13 @@
     "_optional": [
       "goto_synthesizer"
     ],
+    "_nullable": [
+      "rustc",
+      "cbmc",
+      "goto_cc",
+      "goto_instrument",
+      "goto_synthesizer"
+    ],
     "kani": "0.67.0",
     "rustc": "rustc 1.95.0-nightly (838709580 2026-02-17)",
     "cbmc": "6.10.0 (cbmc-6.10.0)",
@@ -116,6 +123,18 @@
         "_optional": [
           "error"
         ],
+        "_nullable": [
+          "total_properties",
+          "passed",
+          "failed",
+          "unreachable",
+          "undetermined",
+          "solver_error",
+          "satisfied",
+          "unsatisfiable",
+          "covered",
+          "uncovered"
+        ],
         "total_properties": 1,
         "passed": 1,
         "failed": 0,
@@ -137,14 +156,34 @@
       ],
       "harness_id": "example_harness",
       "cbmc_metadata": {
+        "_nullable": [
+          "version",
+          "os_info"
+        ],
         "version": "6.7.1",
         "os_info": "x86_64 linux unix"
       },
       "configuration": {
+        "_nullable": [
+          "object_bits",
+          "solver"
+        ],
         "object_bits": 16,
         "solver": "Cadical"
       },
       "cbmc_stats": {
+        "_nullable": [
+          "runtime_symex_s",
+          "size_program_expression",
+          "slicing_removed_assignments",
+          "vccs_generated",
+          "vccs_remaining",
+          "runtime_postprocess_equation_s",
+          "runtime_convert_ssa_s",
+          "runtime_post_process_s",
+          "runtime_solver_s",
+          "runtime_decision_procedure_s"
+        ],
         "runtime_symex_s": 0.005,
         "size_program_expression": 150,
         "slicing_removed_assignments": 80,
diff --git a/tests/json-handler/validator-negative/build_fixtures.py b/tests/json-handler/validator-negative/build_fixtures.py
index f6363638be5..c9eea82eedc 100755
--- a/tests/json-handler/validator-negative/build_fixtures.py
+++ b/tests/json-handler/validator-negative/build_fixtures.py
@@ -71,6 +71,65 @@ def main():
     summary["failed"] = 0
     write(out_dir, "malformed_complete_with_empty_results.json", complete_with_empty_results)
 
+    # The nulls that `--export-json` legitimately emits on degraded runs -- these must
+    # *validate*, not be rejected. Each mirrors a real degraded case the schema's `_nullable`
+    # markers were added for.
+
+    # A harness that timed out or was OOM-killed before its properties were ever counted: the
+    # exporter reports the counts as `null`, not `0`, so a degraded run is never mistaken for
+    # "nothing failed".
+    nullable_timeout = copy.deepcopy(valid)
+    counts = nullable_timeout["property_details"][0]["property_details"]
+    for field in (
+        "total_properties",
+        "passed",
+        "failed",
+        "unreachable",
+        "undetermined",
+        "solver_error",
+        "satisfied",
+        "unsatisfiable",
+        "covered",
+        "uncovered",
+    ):
+        counts[field] = None
+    counts["error"] = "harness timed out before properties were measured"
+    write(out_dir, "nullable_timeout.json", nullable_timeout)
+
+    # An `--smt2` run names no solver and has no notion of object bits.
+    nullable_smt2 = copy.deepcopy(valid)
+    configuration = nullable_smt2["cbmc"][0]["configuration"]
+    configuration["solver"] = None
+    configuration["object_bits"] = None
+    write(out_dir, "nullable_smt2.json", nullable_smt2)
+
+    # Partial `cbmc_stats`: some statistics are unavailable (e.g. the run never reached the
+    # decision procedure), while the rest of the stats are still reported normally.
+    nullable_partial_stats = copy.deepcopy(valid)
+    cbmc_stats = nullable_partial_stats["cbmc"][0]["cbmc_stats"]
+    cbmc_stats["runtime_solver_s"] = None
+    cbmc_stats["vccs_remaining"] = None
+    cbmc_stats["runtime_decision_procedure_s"] = None
+    write(out_dir, "nullable_partial_stats.json", nullable_partial_stats)
+
+    # Failed version/info probes: the tool ran, but querying its version failed.
+    nullable_missing_versions = copy.deepcopy(valid)
+    tools = nullable_missing_versions["tools"]
+    tools["rustc"] = None
+    tools["cbmc"] = None
+    tools["goto_cc"] = None
+    tools["goto_instrument"] = None
+    cbmc_metadata = nullable_missing_versions["cbmc"][0]["cbmc_metadata"]
+    cbmc_metadata["version"] = None
+    cbmc_metadata["os_info"] = None
+    write(out_dir, "nullable_missing_versions.json", nullable_missing_versions)
+
+    # A negative fixture proving `_nullable` is targeted, not blanket: a `null` in a field the
+    # schema does *not* mark nullable must still be rejected.
+    null_in_required_field = copy.deepcopy(valid)
+    null_in_required_field["verification_results"]["summary"]["executed"] = None
+    write(out_dir, "null_in_required_field.json", null_in_required_field)
+
 
 if __name__ == "__main__":
     main()
diff --git a/tests/json-handler/validator-negative/test.sh b/tests/json-handler/validator-negative/test.sh
index 6b059e59024..c7b2c85548c 100755
--- a/tests/json-handler/validator-negative/test.sh
+++ b/tests/json-handler/validator-negative/test.sh
@@ -57,5 +57,28 @@ if python3 "$VALIDATOR" "$WORK_DIR/malformed_complete_with_empty_results.json";
     exit 1
 fi
 
+echo ""
+echo "Checking a degraded export (timed-out harness, property counts: null) still validates..."
+python3 "$VALIDATOR" "$WORK_DIR/nullable_timeout.json"
+
+echo ""
+echo "Checking a degraded export (--smt2 run, no solver/object_bits) still validates..."
+python3 "$VALIDATOR" "$WORK_DIR/nullable_smt2.json"
+
+echo ""
+echo "Checking a degraded export (partial cbmc_stats) still validates..."
+python3 "$VALIDATOR" "$WORK_DIR/nullable_partial_stats.json"
+
+echo ""
+echo "Checking a degraded export (failed tool/CBMC version probes) still validates..."
+python3 "$VALIDATOR" "$WORK_DIR/nullable_missing_versions.json"
+
+echo ""
+echo "Checking a malformed export (verification_results.summary.executed: null) is rejected..."
+if python3 "$VALIDATOR" "$WORK_DIR/null_in_required_field.json"; then
+    echo "ERROR: validator accepted a null in a non-nullable required field"
+    exit 1
+fi
+
 echo ""
 echo "All validator negative-test checks passed"