RFC: Structured verification results (export-json)

[ivmat]

RFC for --export-json <path> — an opt-in, -Z-gated flag that writes one machine-readable file describing a verification run: per-harness status, failed properties, cover and check outcomes, and the provenance needed to reproduce the run.

Why. Today the only way a program can read Kani's results is to grep rendered text for VERIFICATION:- , ** N of M cover properties satisfied, and Verification Time:. Those are printing details, not an interface — when they change, a consumer's grep silently matches nothing.

The specific gap: a proof can pass while proving nothing, and no machine-readable signal says so. A contradictory kani::assume makes every assertion unreachable; the harness reports VERIFICATION:- SUCCESSFUL and exits 0. Kani's text output says ** 0 of 2 failed (2 unreachable) — a program reading the exit code sees a clean proof. This RFC's schema makes that distinction, and the vacuity ones like it, machine-readable.

Why not --sarif. SARIF is findings-shaped: Kani's writer skips cover properties and emits nothing for successful ones, so a fully green run produces an empty results array. Proof, cover and vacuity semantics would have to live in properties bags — a private schema wearing a standard schema's clothes — and --sarif must stay valid SARIF while this artifact must be free to change shape under -Z. One file cannot be both.

Relation to #4472. @yimingyinqwqq proposed this capability there and did substantial work; the design discussion on that PR shaped this proposal, and I'd genuinely welcome their review. This RFC takes 0016 rather than 0015 to leave that PR's number with it. Written RFC-first because that is what reviewers asked for on #4472.

Status. Implemented as a proof of concept; the schema example in the RFC is real output. Happy to open the implementation PR alongside, or keep this standalone — whichever you prefer.

What is deliberately excluded, and why

• CBMC statistics (symex time, VCC counts, solver time) — available only inside CBMC's free-text messages. Extracting them means pattern-matching human-readable output, which is the fragility this RFC exists to remove; doing it inside the fix would be self-defeating.
• Per-harness peak memory — prototyped via getrusage(RUSAGE_CHILDREN) and rejected: ru_maxrss is a process-wide running maximum, so any figure is order-dependent (only a harness that out-peaks all its predecessors gets one) and meaningless under --jobs. Honest measurement needs per-child accounting (wait4()-based rusage or a per-child cgroup) — future work, sketched in the RFC. CI consumers infer OOM from exit code 137 today.
• A stable schema — deferred. The shape is a one-way door, so it stays behind -Z with an explicit schema_version until real consumers have exercised it.

Open questions I'd like input on

1. Should a JSON Schema document ship alongside? That likely means a schemars dependency, which is not currently in the workspace — a real dependency decision rather than something to slip in.
2. Should this cover the autoharness subcommand, or is that a follow-up once the harness-level shape settles?
3. Coverage results (--coverage) — include here, or leave in their existing artifact? (Today code_coverage properties are outside checks/covers and outside n_properties, so the partition invariant holds; a dedicated bucket is the alternative.)
4. configuration now records assertion_reach_checks, ignore_global_asm and extra_pointer_checks — the soundness-relevant toggles we identified. What other options merit the same treatment, and should there be an explicit policy for when a flag must be recorded?

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

[ivmat]

sorry for spamming, but this would help a lot with automatization and it seems previous PR stalled