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.

[ivmat]

@feliperodri thank you for detailed review of the PR. i admit i did not take all things into account, i wanted to start discussion in order to get faster feedback - which i got so thats great. i will fix all the comments, but just need one decision: should we aim for compelete version, i.e intial format to be stable but flexible (but strict per version)? meaning it comes with a schema and revision -- not a problem, just wondering. most of the added details are due to issues i experienced in rs-verified-der so for sure i may have missed some big things simply not having the need for them. so in short, how large coverage do you want from v1, model the full result or just a minimum as first revision. i dont mind which one but this raises another question - if we go for "full" format, could we do implementation in few PRs, simply due to possible size of work (if we go for all items included)?

[feliperodri]

@ivmat we don’t need a full follow-up version here. Since PR #4472 has already been merged and this change is the first version, we can capture the remaining work as open questions or follow-up issues tied to this work/RFC rather than expanding the scope of this PR.

[ivmat]

@feliperodri ok i will then split enhancemnts into issues with each PR (or you want one issue delivery covering them all with one PR?)

[ivmat]

@feliperodri misundestood, thoguht id have to discard this pr -- but now i understand this should stay PR for the RFC.

changes requested from this review:

1. --sarif alternatives — reworked to argue on format grounds, conceding SARIF 2.1.0 could carry this and that skipping covers/successes is our writer's choice, so it no longer invites "then fix the writer."
2. Enum domains — outcome.kind, verdict, and failure_kind now have explicit value-domain tables (with a failure_kind truth table) instead of appearing only by example.
3. schema_version — a new Compatibility policy section defines minor vs major changes and the "consumers must ignore unknown fields" rule.
4. Official 0015 — renumbered 0016 → 0015 and fixed the SUMMARY.md nav gap; left Add --export-json for structured verification results #4472's own 0015 file to you.
5. Sorted harnesses[] — now specified as sorted by (crate_name, file, line, name), so --jobs N output is stable and diffable.
6. --only-codegen — now explicitly rejected, like --sarif.
7. Vacuity predicate — stated exactly, with a note on the partial-vacuity case it misses.
8. warnings — declared outside the schema_version guarantees and bounded with explicit truncation markers.
9. Flag name / stdout — added a --export-json vs --results-json rationale (name left open) and explicitly declined --as-stdout.
10. Curated flag-list — enabled_unstable_features (sorted -Z) is now recorded; a full resolved argv is not, so flag it if you want that.

extra changes:

1. Cut v1 to the core (applying your --export-json: a failed, empty, or partial run can serialize as a clean pass #4731 steer) — dropped cbmc_stats, the auxiliary tool/solver provenance (tools.goto_cc/goto_instrument/goto_synthesizer, tools.solvers[]), the machine block, and object_bits, keeping tools.kani/rustc/cbmc and per-harness resolved_solver, each deferred to Out-of-scope with a tracking-issue note.
2. Honest caveat on that cut — it drops external-solver binary versions, so a solver upgrade that flips an UNDETERMINED is no longer captured (named as the restore trigger in Future work).
3. Completeness is now a 4-value run_state with a pre-verification INCOMPLETE marker — a deliberate change from the rename-only contract, because rename alone leaves a stale prior COMPLETE file readable if a re-run dies during build (marker vs your up-front delete left as an open question).
4. crate_name added, join key (crate_name, name) — fixes cross-workspace misattribution, but differs from --export-json: a failed, empty, or partial run can serialize as a clean pass #4731's mangled_name suggestion, which the RFC explicitly declines.
5. is_bounded mandatory on every harness — a bounded result read as unrestricted is the over-claim that bit a downstream consumer, so it's non-optional.
6. Semantic apparatus added (presence matrix, value-domain tables, counting identities) — this is the "no leaf-value validation" answer at the spec level, with a shippable JSON Schema still an open question.
7. name is the selector — no separate selector field, since the re-run string is pretty_name.
8. Structure — normative tables moved to an appendix to roughly halve the read body (editorial only).

if anything of extra things should be removed, no problem.