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

[feliperodri]

Thanks, thanks, thanks! Thanks for writing this up! This is a genuinely well-constructed RFC, and I appreciate that the motivation is grounded in things that actually exist in the tree rather than hypotheticals. I checked the claims and they hold up: the TODO at kani-driver/src/cbmc_property_renderer.rs:190, update_properties_with_reach_status at cbmc_property_renderer.rs:624, the --output-format=old mocking path at call_cbmc.rs:92, the SARIF writer skipping covers and successes (sarif.rs:143 and sarif_level() at sarif.rs:233), and the kebab-case keys in list/output.rs:113. The exhaustive property bucketing, the atomic-write contract, and the "null never means a guess" discipline are all more carefully specified than most RFCs in this directory.

I'm not asking you to change the design. What I'd like resolved before merge is interface
completeness and one piece of sequencing:

1. The --sarif alternatives section needs to argue on different grounds — see my inline comment.
2. The enum domains (outcome.kind, verdict, failure_kind) need to be specified, not just shown by example.
3. schema_version needs a compatibility policy and stabilization criteria attached to it.
4. Process: #4472 still carries its own rfc/src/rfcs/0015-json-handler.md. Let's make this one the official RFC.

The rest of my comments are smaller and can be resolved in the same pass. Once these are addressed I'm happy to see this merged as Under Review and move on to reviewing the implementation.

[feliperodri]

This is the section I'd most like reworked, because as written it invites exactly the objection you're trying to close off...

Two of the three bullets describe our writer, not the format. Skipping covers is a choice at
kani-driver/src/sarif.rs:143, and the empty-results-on-green behaviour comes from sarif_level() at
sarif.rs:233 returning None for everything except Failure/Undetermined/Unknown. SARIF 2.1.0 itself has result.kind ∈ {pass, fail, informational, notApplicable, review, open} and property bags, so a reviewer can reasonably answer "then fix the writer" to both points. Worth noting too that --sarif is already in main and is not -Z gated, so the bar for a second machine-readable artifact is higher than it would have been a release ago.

I think the argument you want is about consumer contracts rather than expressive power:

• The same file is consumed by code-scanning tools that specifically do not want proof, cover and
  vacuity rows; adding them degrades that consumer to serve a different one.
• --sarif is stable and must stay valid SARIF; this artifact must be free to break shape while it's
  -Z gated. That's the load-bearing point and it's currently the third bullet (I'd lead with it).
• Vacuity has no native SARIF representation, only a property bag, which is a private schema wearing a
  standard schema's clothes (you already say this so it survives the rewrite).

Could you also add a sentence on how the two artifacts avoid drifting apart? If both are derived from
one internal result structure that's a strong answer and worth stating explicitly; if they're
independent renderers, say so and say why that's acceptable.

[feliperodri]

You're admirably rigorous about the property buckets, exhaustive by CBMC status, with an explicit
other catch-all so a consumer never has to guess where an unrecognised result went (lines 219–225).
I'd like the same treatment for the enums introduced here, which currently appear only by example:

• outcome.kind — "COMPLETED" here, "OUT_OF_MEMORY" referenced at line 397. What's the full set?
  I'd expect it to track ExitStatus (Timeout, OutOfMemory, Other) plus the completed and
  never-started cases, but a consumer shouldn't have to reverse-engineer that from call_cbmc.rs.
• outcome.verdict — "SUCCESS" here; presumably a failure counterpart, and possibly an absent/null
  case when the harness didn't complete.
• failure_kind — "NONE" at line 175; this looks like it maps to FailedProperties, so please
  enumerate it and say whether a catch-all applies.

Same question as for the buckets: is each of these closed, or does an unknown value get a catch-all? A
consumer writing an exhaustive match needs to know which.

Minor and related: the keys are snake_case but these values are SCREAMING_SNAKE. Your snake_case
rationale (lines 313–320) rests on reusing kani_metadata and cbmc_output_parser types, which
doesn't extend to these, they look like new types. Either justify the mixed convention or make it
uniform.

[feliperodri]

There's a version field but no rules attached to it, and for an RFC whose whole subject is an
interface, that's the gap I'd most want closed. Could you add a short "Compatibility policy"
subsection covering:

• What is a minor change vs. a breaking one? (I'd expect: adding a field or a new enum variant into an
  existing catch-all is minor; renaming, removing, or changing the meaning of a field is major.)
• What must a consumer do to be forward-compatible? Explicitly stating "consumers must ignore unknown
  fields" is worth a line, because it's the difference between us being able to extend the schema and
  not.
• What should a consumer do on an unknown major? Refuse to parse, presumably... then say so.
• Is warnings inside or outside these guarantees? (See my separate comment; I think outside.)

And separately, per RFC 0006's stabilization section and the template's note that open questions must
be closed before stabilization: what has to be true before this leaves -Z? Even a three-bullet
checklist ("open questions resolved, N releases of consumer feedback, schema doc shipped or explicitly
declined") gives the next person a decision procedure instead of a judgement call.

[feliperodri]

I appreciate the courtesy here, but let's add here as 0015. I'll take care of #4472

[feliperodri]

Not a blocker but... I'd rather this were answered in the RFC than shipped as an open question, because the curated-list
approach has a failure mode the RFC doesn't name: a flag added later that changes result meaning is
silently absent from files written before someone notices, and there's nothing in the artifact to
indicate the omission. That's the same class of silent failure you're arguing against in the
motivation.

The alternative I don't see discussed: record the resolved effective argument set (you already carry
enabled_unstable_features and cbmc_args, so this is an extension rather than a new idea), and keep
the curated configuration.checks block as a convenience view over it. Consumers that want a specific
toggle read the named field; consumers that need to know two runs weren't comparable can diff the
whole set.

If you'd rather stay curated, that's defensible but then please state the policy in the RFC rather
than leaving it open: any flag that changes which properties are generated, or changes what a status
means, must be recorded here. That gives future PRs a test to apply.

[feliperodri]

Vacuity is the RFC's headline motivation, and the example does make it visible, but a consumer still has to infer the rule from the example. Since a harness-level triviality flag is deliberately future work (line 383, and RFC 0003 already frames the concern), I'd like the RFC to state the exact predicate a consumer should apply, e.g. along the lines of checks.total > 0 && checks.success == 0 && !checks.unreachable.is_empty() whatever you consider correct.

Two reasons this is worth the paragraph. First, if every consumer derives its own rule, they'll derive subtly different ones and we'll get bug reports about it. Second, whatever the rule is, it's invalid when configuration.checks.assertion_reach_checks is false; you explain exactly why at lines 250–256, so tying the two together closes the loop and makes the schema self-documenting on its own central claim.

[feliperodri]

I'm fine with carrying these, and the "opaque, do not pattern-match" framing is the right one. Two things to add:

1. State that warnings is outside the schema_version compatibility guarantees. The field's presence and shape are contractual, its contents are not. Otherwise a consumer can reasonably read the version promise as covering it.
2. Size. Your own example is ~11.6 KB for a single warning. Multiply by the standard-library-scale runs this RFC is explicitly targeting (line 40) and the artifact can plausibly become larger than everything else in it combined, which is a problem for the CI consumers that are the whole point. Worth specifying a per-warning cap or per-harness limit with an explicit truncation marker, so a consumer can tell "no more warnings" from "we stopped recording".

[feliperodri]

Not your doing, but visible in your diff: 0014-harness-partition never got a SUMMARY.md entry when it landed (#4228), so with your line added the book navigation reads 0013 → 0016. Could you fix
it as a drive-by here?

[feliperodri]

Two small things on the surface syntax:

• Every other artifact-producing flag we have is a noun: --sarif <PATH>, --output-into-files. --export-json is a verb and doesn't say what's being exported — next to --sarif on a command line, something like --results-json <PATH> reads better and ages better if we ever emit a second JSON artifact. Not a hill I'll die on, but worth one paragraph in the rationale either way.
• Worth also supporting - for stdout, or explicitly declining to; piping into a consumer without a temp file is a natural CI want, and it interacts with your atomic-write contract, so it's better settled in the RFC than discovered later.
• Could you justify a dedicated -Z export-json over -Z unstable-options? Both patterns exist in the tree (--coverage gates on SourceCoverage; most plain options gate on UnstableOptions), and the template's footnote implies a per-RFC ident, so I think you're fine and I'd just like the choice stated rather than implied.

[feliperodri]

This paragraph is the best part of the RFC! 🤩 The rename-based "exists implies complete" contract, the explanation of why the up-front delete is additionally needed, and the enumeration of what absence can and cannot distinguish. I hope we can keep this level of precision when the implementation PR lands; it's exactly the reasoning that's usually missing from output-format work.