Add --export-json for structured verification results

[yimingyinqwqq]

Add opt-in JSON export (--export-json ) to emit structured verification results (metadata, per-harness outcomes, CBMC stats).
Improves Kani by enabling reliable machine-readable output for external tools and applications.

Context: Current output is human-readable only, which blocks robust automation and integrations.

Manual tests:
• Run cargo kani --export-json out.json
• With multiple harnesses: counts in summary match executed harnesses.

Resolves #2572

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

Copilot reviewed 27 out of 27 changed files in this pull request and generated no new comments.

Suppressed comments (11)

kani-driver/src/args/mod.rs:248

• --export-json needs conflict validation for modes that cannot produce a real export. With --only-codegen, verify_project is skipped and the command succeeds without creating the requested file; with --output-format=old, run_cbmc constructs a mock VerificationResult, so the JSON can report a fabricated success with no checks. Reject these combinations, as is already done for SARIF.

    /// 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>,

kani-driver/src/frontend/schema_utils.rs:46

• This exports the artifact output directory as workspace_root. Project::outdir is explicitly the compiler output directory (project.rs:33-37), and for Cargo it points under target/.../debug/deps, not to the workspace. Use Cargo metadata's workspace_root for Cargo projects and define the standalone equivalent from the input source path.

    "workspace_root": project.outdir.clone(),

kani-driver/src/frontend/schema_utils.rs:255

• These values do not reliably describe the CBMC invocation. cbmc_object_bits() returns None when --object-bits is supplied through --cbmc-args, and the solver ignores session.args.solver, even though that option takes precedence over harness attributes in call_cbmc.rs:425-431. Export the same effective configuration used to build the command so consumers do not receive null/Cadical for explicitly configured runs.

                "object_bits": session.args.cbmc_object_bits(),
                "solver": h.attributes.solver.as_ref().map(|s| format!("{:?}", s)).unwrap_or_else(|| "Cadical".to_string()),

kani-driver/src/main.rs:195

• The PR marks coverage issue #2636 as resolved, but the export only records whether coverage was enabled; none of the per-harness coverage_results are serialized, and the existing user-facing coverage output is unchanged. Export the coverage outcomes or remove the issue-closing claim.

    if let Some(handler) = handler.as_mut() {
        handler.add_item("coverage", json!({"enabled": session.args.coverage}));
        handler.export()?;

kani-driver/src/frontend/schema_utils.rs:224

• For timeout, OOM, or another CBMC execution error, this object omits passed, failed, unreachable, and undetermined, although the bundled schema marks all four as required. Such exports therefore fail the new validator. Keep the shape stable and represent unavailable counts explicitly (or mark them optional in the schema).

                    Err(_) => json!({
                        "total_properties": 0,
                        "error": "Could not extract property details due to verification failure"
                    })

scripts/validate_json_export.py:85

• Only validating element zero lets malformed data in every later harness/result pass schema validation. Iterate over every array element against the item template so multi-harness exports are actually covered.

            # Validate first item against schema template
            sub_errors = validate_structure_recursive(data[0], schema[0], f"{path}[0]")[
                1
            ]
            errors.extend(sub_errors)

scripts/validate_json_export.py:87

• The validator performs no scalar type validation, and a schema object paired with a non-object also falls through here successfully. Consequently fields such as metadata, numeric counts, and booleans can have invalid JSON types while the “schema validation” passes. Encode expected and nullable types (ideally with JSON Schema) and reject type mismatches.

    # Leaf values - no validation needed

tests/json-handler/basic-export/test.sh:7

• Without pipefail, a nonzero validator exit is hidden by the successful tail, so this integration test passes even when schema validation fails. Enable pipeline failure propagation.

set -eu

tests/json-handler/multiple-harnesses/test.sh:7

• Without pipefail, a nonzero validator exit is hidden by the successful tail, so this integration test passes even when schema validation fails. Enable pipeline failure propagation.

set -eu

kani-driver/src/main.rs:149

• The PR description also declares unrelated issues resolved (for example #1219's compiletest --help panic and #3357's non-terse parallel output), but this change does not touch those paths and the existing non-terse parallel restriction remains. Remove the unrelated Resolves entries to avoid closing still-open problems.

    // 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())));

tests/json-handler/multiple-harnesses/test.sh:37

• This test only counts metadata entries, so it does not verify the aggregation behavior stated in the PR (summary counts matching executed harnesses). Assert the results length and all summary counters for the three successful harnesses.

HARNESS_COUNT=$(python3 -c "import json; data=json.load(open('$OUTPUT_FILE')); print(len(data['harness_metadata']))")

[Copilot]

Pull request overview

Copilot reviewed 27 out of 27 changed files in this pull request and generated no new comments.

Suppressed comments (5)

kani-driver/src/harness_runner.rs:115

• With --fail-fast, this vector contains only the failing harness. Any successful harnesses executed before the failure are discarded by the collect::<Result<Vec<_>>>() above, so the exported executed count becomes 1 and those real executions disappear from results. Preserve completed results (including the failure) when building the fail-fast report so the machine-readable summary reflects what actually ran.

                    let result = vec![HarnessResult {
                        harness: sorted_harnesses[failed.index_to_failing_harness],
                        result: failed.result,
                    }];

kani-driver/src/frontend/schema_utils.rs:224

• The exported property totals cannot be reconciled for valid CBMC statuses. CheckStatus also includes Unknown, Error, Covered, Uncovered, Satisfied, and Unsatisfiable; none are counted here (and Unknown, which Kani renders as undetermined, is omitted from undetermined). As a result, these category counts can sum to less than total_properties. Export every status or define an exhaustive grouping so consumers do not receive incomplete statistics.

                        json!({
                            "total_properties": properties.len(),
                            "passed": count(CheckStatus::Success),
                            "failed": count(CheckStatus::Failure),
                            // Counted directly rather than derived by subtraction, which silently
                            // reported undetermined and error properties as unreachable.
                            "unreachable": count(CheckStatus::Unreachable),
                            "undetermined": count(CheckStatus::Undetermined)
                        })

kani-driver/src/frontend/schema_utils.rs:290

• This can report the wrong solver when users select one through the supported --cbmc-args escape hatch (for example, --cbmc-args --sat-solver minisat). Those arguments are appended after Kani's generated solver flags, but resolved_solver only considers --solver, the harness attribute, and the default. Resolve direct CBMC solver arguments too, or reject them with --export-json, so configuration.solver describes the command that actually ran.

            "configuration": {
                "object_bits": effective_object_bits(session),
                "solver": format!("{:?}", session.resolved_solver(&h.attributes.solver)),
            },

kani-driver/src/args/mod.rs:248

• The PR description marks several unrelated issues as resolved, including #1219 (a compiletest --help panic), #2636 (human-friendly coverage output), and #3357 (parallel non-terse output), but this option and the accompanying changes do not implement those requests. Remove the unrelated Resolves entries or implement their acceptance criteria; otherwise merging this PR will incorrectly close open work.

    /// 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>,

scripts/validate_json_export.py:90

• The validator never checks leaf types or values, so malformed exports such as string summary counts, numeric status values, or null metadata pass as long as the keys exist. That means the new integration tests do not actually validate the structured contract represented by the template. Validate primitive types (and fixed enum/version values where applicable), or use a real JSON Schema validator.

    # Leaf values - no validation needed

[feliperodri]

Two comments I'm deliberately not acting on in this PR

Both are legitimate, but both are decisions for RFC #4727 rather than fixes:

Type validation / adopting a real JSON Schema. Correct that the current validator does no scalar
type checking, so a numeric count could be a string and validation would still pass. But "ideally
with JSON Schema" is precisely the open question in RFC 0016: shipping a schema document implies a
schemars dependency that isn't in the workspace today, which is a real dependency decision rather
than something to add quietly. Anything homegrown I write here gets thrown away when that's settled,
so I'd rather leave the gap documented than build a second half-validator. Happy to do it either way
if reviewers prefer type checks in the interim.

Exporting coverage results. Also correct that the export only records whether coverage was
enabled and serializes none of the per-harness coverage_results. RFC 0016 lists "coverage results —
include here, or leave with kani-cov?" as an open question and defers aggregate coverage to
kani-cov and RFC 0011. Settling it inside an implementation PR would pre-empt the RFC, so the fix
here is to stop claiming it: the Resolves #2636 line is going away with the PR description rewrite,
along with the other issue-closing claims that don't hold — #1219 (compiletest --help panic) and
#3357 (non-terse parallel output) aren't touched by this change either, and the non-terse parallel
restriction is still in place. The description will say Tracks #942 and nothing more.

Three comments that don't hold

Flagging these so they don't get re-raised:

• JsonHandler::export using ? on serde_json::to_string_pretty compiles fine — serde_json
  provides impl From<serde_json::Error> for std::io::Error. The suggested
  io::Error::new(io::ErrorKind::Other, e) would also be a step back, since ErrorKind::Other is
  discouraged for this and io::Error::other exists.
• create_harness_metadata_json and create_verification_result_json do not move owned Strings
  out of a borrow: json! serializes through to_value(&expr). Adding & is a no-op.
• The basic-export cleanup trap was already added in 5d23989, which the suggestion notes as
  outdated.

The branch builds clean and passes cargo clippy --workspace --tests -- -D warnings, both clippy
passes, cargo test -p kani-driver, and the json-handler (4), ui (144) and coverage (20)
suites locally.

[Copilot]

Pull request overview

Copilot reviewed 27 out of 27 changed files in this pull request and generated 2 comments.

Suppressed comments (4)

kani-driver/src/frontend/schema_utils.rs:96

• tools.solvers ignores solver overrides passed through --cbmc-args. Those arguments are appended after Kani's solver flags (call_cbmc.rs:357), and this file already resolves them for cbmc[].configuration.solver, so an invocation such as --solver cadical --cbmc-args --z3 exports contradictory metadata: Cadical here but Z3 in the per-harness configuration and actual run. Derive the version probes from the same effective-solver resolution, including --external-sat-solver.

        let (name, binary) = match session.resolved_solver(&harness.attributes.solver) {

kani-driver/src/harness_runner.rs:122

• With --fail-fast, result contains only the failing harness because the Result<Vec<_>> collection discarded any successful results completed before the error. Serializing this singleton makes summary.executed, successful, duration_ms, and the per-harness arrays underreport what actually ran (especially with parallel jobs). Preserve completed results through the fail-fast path before generating the JSON summary.

                        add_runner_results_to_json(
                            handler,
                            &result,
                            harnesses.len(),
                            "completed_with_fail_fast",

scripts/validate_json_export.py:52

• When the template expects an object but the exported value is not an object, this condition falls through to the leaf case and reports success. For example, {"metadata": null, ...} bypasses every required metadata field, so the schema tests can accept structurally malformed exports. Reject object type mismatches and explicitly model the few fields that are legitimately nullable.

    # Handle dict validation
    if isinstance(schema, dict) and isinstance(data, dict):

tests/json-handler/basic-export/test.sh:21

• All new end-to-end scripts invoke standalone kani; none exercises the advertised cargo kani --export-json path. That leaves Cargo argument handling and Cargo-only project metadata such as workspace_root unverified. Add a cargo-kani integration case that exports and validates a small Cargo project.

# Run Kani with JSON export
kani -Z unstable-options test.rs --export-json "$OUTPUT_FILE"

[Copilot]

Pull request overview

Copilot reviewed 30 out of 30 changed files in this pull request and generated no new comments.

Suppressed comments (3)

kani-driver/src/frontend/schema_utils.rs:269

• pretty_name is crate-relative (readable_name strips the local crate prefix), so two crates in one workspace can expose the same harness name. Using it as harness_id makes the export ambiguous and also causes the later find calls keyed only by pretty_name to attach both crates' details to the first matching result. Use a globally unique identifier, such as a crate-qualified name, consistently across metadata, results, and detail arrays.

        "harness_id": result.harness.pretty_name,  // Reference to harness instead of duplicating name

kani-driver/src/harness_runner.rs:115

• This rebuilds the fail-fast output from only the failing harness, but collect::<Result<Vec<_>>>() has already discarded every successful result produced before that failure. Even with --jobs 1, if the second harness fails, the JSON reports executed: 1 and omits the first harness although it ran. Preserve completed results when stopping so the structured summary reflects all executions.

                    let result = vec![HarnessResult {
                        harness: sorted_harnesses[failed.index_to_failing_harness],
                        result: failed.result,
                    }];

kani-driver/src/frontend/schema_utils.rs:48

• A tool that rejects --version but prints an error or usage line to stdout is recorded as having that text as its version. This contradicts the documented null-on-undetermined behavior and can mislead JSON consumers; require a successful exit status before parsing stdout.

    let output = Command::new(binary).arg("--version").output().ok()?;