ivmat · Oct 6, 2026
@@ -185,4 +185,4 @@ cargo kani -Z export-json --export-json kani.json
 
 The file describes the tool versions, the configuration and the outcome of every harness. The format is unstable and may change between releases; see [RFC 0015](https://model-checking.github.io/kani/rfc/rfcs/0015-export-json.html) for the schema. The flag requires `-Z export-json`; `-Z unstable-options` alone is no longer enough.
 
-This version never writes the `INCOMPLETE` marker that the RFC describes. If a run is killed, the file from an earlier run can stay in place and look complete. Compare its `started_at` with the time of your run.
+After a successful build and harness selection, Kani replaces any earlier file with an `INCOMPLETE` marker before verification starts, and replaces the marker with the final document at the end. A killed or failed run can leave the marker. A failure before the marker is written leaves any earlier file in place; compare its `started_at` with the time of your run.
@@ -32,7 +32,7 @@ const KANI_GIT_SHA: Option<&str> = option_env!("KANI_GIT_SHA");
 /// `None` exactly when `KANI_GIT_SHA` is `None`.
 const KANI_GIT_DIRTY: Option<&str> = option_env!("KANI_GIT_DIRTY");
 
-struct RunContext {
+pub(crate) struct RunContext {
     cbmc_version: Option<String>,
     rustc_version: Option<String>,
     kani_commit: Option<&'static str>,
@@ -42,21 +42,29 @@ struct RunContext {
     harness_timeout_s: Option<f64>,
     configuration: ConfigurationExport,
     started_at: OffsetDateTime,
-    wall_time: Duration,
 }
 
 impl KaniSession {
-    /// Writes `--export-json` for a completed run; no-op if unset. `matched_harnesses` must be
-    /// the pre-verification list, not `results`, which `--fail-fast` can truncate.
-    pub fn write_export_json(
+    /// Writes the `--export-json` marker and returns its context; no-op if unset.
+    pub(crate) fn begin_export_json(
         &self,
         matched_harnesses: &[&HarnessMetadata],
-        results: &[HarnessResult<'_>],
         started_at: OffsetDateTime,
+    ) -> Result<Option<RunContext>> {
+        let Some(path) = &self.args.export_json else { return Ok(None) };
+        let ctx = self.build_run_context(matched_harnesses, started_at);
+        write_json_atomically(path, &IncompleteRun::from(&ctx))?;
+        Ok(Some(ctx))
+    }
+
+    /// Writes the terminal `--export-json` document; no-op if unset.
+    pub fn write_export_json(
+        &self,
+        results: &[HarnessResult<'_>],
+        ctx: Option<RunContext>,
         wall_time: Duration,
     ) -> Result<()> {
-        let Some(path) = &self.args.export_json else { return Ok(()) };
-        let ctx = self.build_run_context(matched_harnesses, started_at, wall_time);
+        let (Some(path), Some(ctx)) = (&self.args.export_json, ctx) else { return Ok(()) };
         let export = ExportedRun::from_harness_results(
             results,
             |harness| {
@@ -67,6 +75,7 @@ impl KaniSession {
                 )
             },
             ctx,
+            wall_time,
         );
         write_json_atomically(path, &export)
     }
@@ -75,7 +84,6 @@ impl KaniSession {
         &self,
         matched_harnesses: &[&HarnessMetadata],
         started_at: OffsetDateTime,
-        wall_time: Duration,
     ) -> RunContext {
         let enabled_unstable_features: BTreeSet<String> = self
             .args
@@ -104,7 +112,6 @@ impl KaniSession {
             harness_timeout_s: self.args.harness_timeout.map(|t| Duration::from(t).as_secs_f64()),
             configuration: configuration_from(&self.args),
             started_at,
-            wall_time,
         }
     }
 }
@@ -287,6 +294,49 @@ struct ToolsExport {
     cbmc: Option<String>,
 }
 
+#[derive(Serialize)]
+struct IncompleteRun<'a> {
+    schema_version: &'static str,
+    kani_commit: Option<&'static str>,
+    kani_commit_dirty: Option<bool>,
+    tools: ToolsExport,
+    enabled_unstable_features: &'a BTreeSet<String>,
+    harness_selection: &'a HarnessSelectionExport,
+    harness_timeout_s: Option<f64>,
+    configuration: &'a ConfigurationExport,
+    run_state: IncompleteState,
+    target: &'static str,
+    started_at: String,
+}
+
+#[derive(Serialize)]
+#[serde(rename_all = "SCREAMING_SNAKE_CASE")]
+enum IncompleteState {
+    Incomplete,
+}
+
+impl<'a> From<&'a RunContext> for IncompleteRun<'a> {
+    fn from(ctx: &'a RunContext) -> Self {
+        Self {
+            schema_version: SCHEMA_VERSION,
+            kani_commit: ctx.kani_commit,
+            kani_commit_dirty: ctx.kani_commit_dirty,
+            tools: ToolsExport {
+                kani: KANI_VERSION,
+                rustc: ctx.rustc_version.clone(),
+                cbmc: ctx.cbmc_version.clone(),
+            },
+            enabled_unstable_features: &ctx.enabled_unstable_features,
+            harness_selection: &ctx.harness_selection,
+            harness_timeout_s: ctx.harness_timeout_s,
+            configuration: &ctx.configuration,
+            run_state: IncompleteState::Incomplete,
+            target: env!("TARGET"),
+            started_at: format_started_at(ctx.started_at),
+        }
+    }
+}
+
 #[derive(Serialize)]
 struct ExportedRun {
     schema_version: &'static str,
@@ -616,6 +666,7 @@ impl ExportedRun {
         results: &[HarnessResult<'_>],
         resolve: impl Fn(&HarnessMetadata) -> (Option<String>, Option<u32>),
         ctx: RunContext,
+        wall_time: Duration,
     ) -> Self {
         let mut harnesses: Vec<HarnessExport> = results
             .iter()
@@ -660,7 +711,7 @@ impl ExportedRun {
             run_state,
             target: env!("TARGET"),
             started_at: format_started_at(ctx.started_at),
-            wall_time_s: ctx.wall_time.as_secs_f64(),
+            wall_time_s: wall_time.as_secs_f64(),
             harnesses,
             summary,
         }
@@ -885,7 +936,6 @@ mod tests {
             harness_timeout_s: None,
             configuration: test_ctx_config(),
             started_at: started(),
-            wall_time: Duration::from_millis(1),
         }
     }
 
@@ -894,13 +944,86 @@ mod tests {
     }
 
     fn export_with(results: &[HarnessResult<'_>], ctx: RunContext) -> ExportedRun {
-        ExportedRun::from_harness_results(results, cadical, ctx)
+        ExportedRun::from_harness_results(results, cadical, ctx, Duration::from_millis(1))
     }
 
     fn export_one(hr: HarnessResult<'_>) -> ExportedRun {
         export_with(&[hr], test_context())
     }
 
+    #[test]
+    fn incomplete_marker_serializes_only_marker_fields() {
+        let mut ctx = test_context();
+        ctx.kani_commit = Some("abc123");
+        ctx.kani_commit_dirty = Some(true);
+        ctx.rustc_version = Some("rustc test".to_string());
+        ctx.cbmc_version = Some("CBMC test".to_string());
+        ctx.enabled_unstable_features.insert("export-json".to_string());
+
+        let marker = serde_json::to_value(IncompleteRun::from(&ctx)).unwrap();
+        let keys: BTreeSet<&str> = marker.as_object().unwrap().keys().map(String::as_str).collect();
+        assert_eq!(
+            keys,
+            BTreeSet::from([
+                "configuration",
+                "enabled_unstable_features",
+                "harness_selection",
+                "harness_timeout_s",
+                "kani_commit",
+                "kani_commit_dirty",
+                "run_state",
+                "schema_version",
+                "started_at",
+                "target",
+                "tools",
+            ])
+        );
+        assert_eq!(marker["run_state"], "INCOMPLETE");
+        assert_eq!(marker["kani_commit"], "abc123");
+        assert_eq!(marker["kani_commit_dirty"], true);
+        assert_eq!(marker["tools"]["rustc"], "rustc test");
+        assert_eq!(marker["tools"]["cbmc"], "CBMC test");
+        let null_marker = serde_json::to_value(IncompleteRun::from(&test_context())).unwrap();
+        assert!(null_marker["kani_commit"].is_null());
+        assert!(null_marker["kani_commit_dirty"].is_null());
+        assert!(null_marker["tools"]["rustc"].is_null());
+        assert!(null_marker["tools"]["cbmc"].is_null());
+    }
+
+    #[test]
+    fn incomplete_marker_and_terminal_export_share_context() {
+        let mut ctx = test_context();
+        ctx.kani_commit = Some("shared-commit");
+        ctx.cbmc_version = Some("shared CBMC".to_string());
+        ctx.enabled_unstable_features.insert("export-json".to_string());
+        let marker = serde_json::to_value(IncompleteRun::from(&ctx)).unwrap();
+
+        let h = harness("h");
+        let hr = HarnessResult { harness: &h, result: success_result(vec![]) };
+        let terminal = serde_json::to_value(ExportedRun::from_harness_results(
+            &[hr],
+            cadical,
+            ctx,
+            Duration::from_millis(500),
+        ))
+        .unwrap();
+
+        for key in [
+            "schema_version",
+            "kani_commit",
+            "kani_commit_dirty",
+            "tools",
+            "enabled_unstable_features",
+            "harness_selection",
+            "harness_timeout_s",
+            "configuration",
+            "target",
+            "started_at",
+        ] {
+            assert_eq!(marker[key], terminal[key], "shared field {key}");
+        }
+    }
+
     #[test]
     fn export_all_successful() {
         let h = harness("my_harness");
@@ -911,12 +1034,9 @@ mod tests {
         let result = success_result(properties);
         let hr = HarnessResult { harness: &h, result };
 
-        let ctx = RunContext {
-            cbmc_version: Some("CBMC 6.8.0".to_string()),
-            wall_time: Duration::from_millis(500),
-            ..test_context()
-        };
-        let export = export_with(&[hr], ctx);
+        let ctx = RunContext { cbmc_version: Some("CBMC 6.8.0".to_string()), ..test_context() };
+        let export =
+            ExportedRun::from_harness_results(&[hr], cadical, ctx, Duration::from_millis(500));
         let v = serde_json::to_value(&export).unwrap();
 
         assert_eq!(v["schema_version"], "0.1.0");
@@ -1797,6 +1917,7 @@ mod tests {
             &[hr],
             |_| (Some("cadical".to_string()), Some(7)),
             test_context(),
+            Duration::from_millis(1),
         ))
         .unwrap();
         let hj = &v["harnesses"][0];
@@ -1936,6 +2057,7 @@ mod tests {
             &[hr],
             |_| (Some("totally-unfamiliar-solver-v9".to_string()), None),
             test_context(),
+            Duration::from_millis(1),
         ))
         .unwrap();
         assert_eq!(v["harnesses"][0]["resolved_solver"], "totally-unfamiliar-solver-v9");

@@ -191,6 +191,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
 
     let harnesses = session.determine_targets(project.get_all_harnesses())?;
     debug!(n = harnesses.len(), ?harnesses, "verify_project");
+    let export_context = session.begin_export_json(&harnesses, started_at)?;
 
     // Verification
     let runner = harness_runner::HarnessRunner { sess: &session, project: &project };
@@ -215,7 +216,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
         session.save_coverage_results(&project, &results, &timestamp)?;
     }
 
-    session.write_export_json(&harnesses, &results, started_at, start_instant.elapsed())?;
+    session.write_export_json(&results, export_context, start_instant.elapsed())?;
     session.write_sarif(&results)?;
     if !session.args.common_args.quiet {
         session.print_final_summary(&results)?;

@@ -244,7 +244,8 @@ Each write puts full JSON in a temporary file in the target directory, then atom
 the target (same-filesystem POSIX rename). A mid-write kill leaves the previous target and possibly an
 orphaned temp file, never a partially written target. After building and selecting harnesses, when
 verification begins, an atomic `INCOMPLETE` marker replaces any earlier file. It contains known
-pre-verification fields, without `outcome`, `wall_time_s`, `summary` or `harnesses[]`.
+pre-verification fields, without `outcome`, `wall_time_s`, `summary` or `harnesses[]`. The marker is also
+written for an empty, unfiltered harness selection before the terminal `NO_HARNESSES_SELECTED` document replaces it.
 First check `schema_version` (refuse unsupported major or, pre-1.0, minor), then `run_state`:
 
 - Only `COMPLETE` is complete verification evidence: every selected harness has an entry, regardless of outcome.
@@ -257,7 +258,7 @@ deletion fails closed on `ENOENT`. Concurrent writers to one path are unsupporte
 `NO_HARNESSES_SELECTED` means an unfiltered project/workspace with no selectable proof harness or eligible
 autoharness function: `requested_filters == []`, `unmatched_filters == []`, `matched_count == 0`.
 A wholly unmatched filter set, or any unmatched `--exact` filter, errors non-zero before export (#4743).
-Nonempty `unmatched_filters` occurs only without `--exact` in `COMPLETE`/`PARTIAL` when another filter matched.
+Nonempty `unmatched_filters` occurs only without `--exact` in `INCOMPLETE`/`COMPLETE`/`PARTIAL` when another filter matched.
 
 ## Rationale and alternatives
 
@@ -420,7 +421,7 @@ The narrower `INCOMPLETE` marker follows its presence matrix below.
 | `run_state` | `"INCOMPLETE"` \| `"COMPLETE"` \| `"PARTIAL"` \| `"NO_HARNESSES_SELECTED"` | — | Trust is based on this field; see Completeness under Reading the results. |
 | `target` | string | — | The Rust target triple Kani itself was built for. |
 | `started_at` | string | — | UTC, `YYYY-MM-DDTHH:MM:SSZ` (second resolution). Taken after the build, when target selection starts. |
-| `wall_time_s` | number | — | Seconds from target selection to the start of the export write: target selection, verification and coverage output. The build is not included. Volatile between runs by design (see "Interaction with other flags"). |
+| `wall_time_s` | number | — | Seconds from target selection to the start of the terminal export write: target selection, the tool version probes and the marker write, verification and coverage output. The build is not included. Volatile between runs by design (see "Interaction with other flags"). |
 | `harnesses[]` | array of harness objects | never null, may be empty (e.g. under `NO_HARNESSES_SELECTED`) | Sorted by `(crate_name, file, line, name)`. |
 | `harnesses[].name` | string | — | Fully qualified `pretty_name`; see Selection under Reading the results. |
 | `harnesses[].crate_name` | string | — | Distinguishes same-named harnesses across crates in one workspace. |

@@ -0,0 +1,3 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: test.sh
@@ -0,0 +1,34 @@
+#!/usr/bin/env python3
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+import json
+import os
+import sys
+import time
+
+
+def main():
+    real_cbmc = os.environ["REAL_CBMC"]
+    if sys.argv[1:] == ["--version"]:
+        os.execv(real_cbmc, [real_cbmc, "--version"])
+
+    ready = os.environ["FAKE_CBMC_READY"]
+    record = {"pid": os.getpid(), "ppid": os.getppid()}
+    temporary = f"{ready}.{os.getpid()}.tmp"
+    with open(temporary, "w", encoding="utf-8") as output:
+        json.dump(record, output)
+    os.replace(temporary, ready)
+
+    deadline = time.monotonic() + float(os.environ.get("FAKE_CBMC_TIMEOUT_S", "25"))
+    release = os.environ["FAKE_CBMC_RELEASE"]
+    while time.monotonic() < deadline:
+        if os.path.exists(release):
+            os.execv(real_cbmc, [real_cbmc, *sys.argv[1:]])
+        time.sleep(0.02)
+    print("fake cbmc timed out waiting for release", file=sys.stderr)
+    return 124
+
+
+if __name__ == "__main__":
+    sys.exit(main())
Original file line number	Diff line number	Diff line change
Expand Up		@@ -185,4 +185,4 @@ cargo kani -Z export-json --export-json kani.json

		The file describes the tool versions, the configuration and the outcome of every harness. The format is unstable and may change between releases; see [RFC 0015](https://model-checking.github.io/kani/rfc/rfcs/0015-export-json.html) for the schema. The flag requires `-Z export-json`; `-Z unstable-options` alone is no longer enough.

		This version never writes the `INCOMPLETE` marker that the RFC describes. If a run is killed, the file from an earlier run can stay in place and look complete. Compare its `started_at` with the time of your run.
		After a successful build and harness selection, Kani replaces any earlier file with an `INCOMPLETE` marker before verification starts, and replaces the marker with the final document at the end. A killed or failed run can leave the marker. A failure before the marker is written leaves any earlier file in place; compare its `started_at` with the time of your run.