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