RFC: Structured verification results (export-json)

[ivmat]

Part A — Normative summary

RFC 0015 proposes a consumer contract for Kani's --export-json <path> output. The flag shipped in #4472 behind -Z unstable-options. This RFC proposes a dedicated -Z export-json gate and a versioned JSON document describing one verification run.

The contract defines:

• Per-harness outcomes, failed properties, and check and cover results grouped by status.
• Tool versions, effective configuration, and harness selection needed to interpret results.
• Vacuity predicates and the settings needed to interpret unreachable assertions.
• Completeness states, atomic file writes, and rules for missing results, failures, and schema compatibility.

Shipped JSON already exposes processed property statuses and unreachable counts. This proposal specifies how consumers should interpret them, including when a successful harness has unreachable assertions and whether the export accounts for every selected harness.

The export complements --sarif, which reports findings for code-scanning tools. The proposed JSON also includes successful-check counts and cover results.

The schema remains unstable. Whether it should replace the shipped v1 shape, and how to resolve the remaining configuration and provenance gaps before stabilization, remain open questions. The RFC example illustrates the proposed schema; it is not captured verification output.

This PR changes documentation only. The RFC file contains the complete normative proposal.

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

---

Part B — Extended reference (informative — not part of the normative RFC)

Part B is informative and is not part of the normative RFC. It preserves the longer explanations and implementation notes moved out of the RFC and adds no normative requirements.

Read the extended reference

Extended reference (informative)

Supporting reference for RFC 0015 / PR #4727.
The RFC contains the proposed contract. This reference preserves explanations, implementation
comparisons and deferred-work detail moved out of it; it adds no normative requirements.
Interim home: a PR body comment. The explanatory material can later be adapted for the Kani book
or implementation documentation. Revision-specific observations below describe those revisions,
not a claim that one implementation already emits the entire proposed schema.

1. Revisions and illustrative example

Source descriptions below use checkout 902daa525. Historical PoC behavior is qualified by
7b125f1b; later upstream behavior from #4717/#4719 is qualified by 10bc1ae04. These revisions have
different capabilities; the proposed schema is not a description of any one of their emitted files.

The RFC output example is an example of the proposed 0015 document, for the vacuity case
the motivation describes: two ordinary assertions made unreachable by one contradictory
kani::assume. The PoC at 7b125f1b47e36ca4cc50c4041abeca01912f80f9 contains a synthetic unit test,
export_checks_unreachable_under_contradictory_assume, that constructs two unreachable assertions and
a successful result. It supports the illustrated result semantics, but is not a captured verification
run. The RFC's harness, provenance, timings, and JSON are illustrative, not a measured run or verbatim
PoC output. That PoC emits flat kani_version/cbmc_version fields (not the grouped tools object) and
a boolean run_complete (not run_state), and lacks is_bounded and
configuration.coverage_enabled. It already has summary and all seven totals; this RFC refines their
treatment of non-completed harnesses, as specified in the RFC.

The marker, warning caps and directory-path validation are proposed changes, not PoC capabilities.
At 902daa525, --fail-fast collects a Result<Vec<_>> and returns only the failing result on
error, discarding other results even if those harnesses completed. The later #4744 fix retains
completed results. Completeness measures reported entries, not which missing harnesses ran.

2. Field explanations and warnings

Tool provenance (tools). The tools object records the versions of the core tools whose behaviour
can change a result: kani itself (always known, so never null), the rustc toolchain kani-compiler
was built against, and cbmc. It is the machine-readable form of the versions Kani already prints,
narrowing the gap in #2572. One rule for the two
probed entries: a version that cannot be determined is null, never guessed — whether the probe
binary is missing, refuses --version, or prints nothing parseable. (An earlier draft also carried
goto_cc/goto_instrument/goto_synthesizer versions and a solvers[] array of every resolved
solver; those are cut from v1 to keep it to the core — see the "Full tool & solver provenance"
future-work item. The solver CBMC actually ran with is still recoverable per harness from
harnesses[].resolved_solver.)

Harnesses that are not --harness-selectable. An is_automatically_generated harness (from kani autoharness) cannot be selected by --harness/--exact at all: find_proof_harnesses skips
generated harnesses regardless of filter. Its name is still reported (a real, unique identifier), but
a consumer must not use it as a --harness argument when is_automatically_generated is true. A
#[kani::proof_for_contract] harness, by contrast, is selectable, and its name is the harness
function's own path — not the target it proves a contract for (that is
attributes.kind.ProofForContract.target_fn, see §7).

Why not mangled_name. HarnessMetadata also carries a mangled_name (the harness's name in
CBMC's symbol table), but this schema does not export it and it would not serve as a selector: it
identifies the harness to CBMC, not to Kani's CLI, and --harness does not accept it. name
(pretty_name) is chosen because it is simultaneously human-readable, module-qualified, and directly
re-runnable.

checks/covers bucket every included property exhaustively by CBMC status. This partition and
n_properties cover exactly what they bucket; code_coverage (COVERED/UNCOVERED) properties under
--coverage are outside both and n_properties (no dedicated place today), so n_properties == checks.total + covers.total holds on a COMPLETED harness. checks.success is a bare count, unlike every other bucket: successful-check
identities are numerous and of little value, whereas covers.satisfied names its properties because covers
are user-authored and few. Exporting successful-check identities is future work.

The checks / covers partition criterion. A property goes into covers exactly when
property_id.class == "cover" (Property::is_cover_property, kani-driver/src/cbmc_output_parser.rs);
every property whose class is neither "cover" nor "code_coverage" goes into checks (including
"assertion", which carries ordinary assert!/panic checks). This is a syntactic test on the
CBMC-assigned class, independent of status: a cover-class property carrying a status normally seen
among checks (or vice versa) still partitions by class and is recorded in that domain's other[] array
rather than crossing over (see the RFC’s Value domains). code_coverage-class properties are excluded from both buckets entirely.

failed_properties[] membership. failed_properties[] names exactly the properties in
checks.failure (class is neither "cover" nor "code_coverage", with status == "FAILURE"), with
the full per-property shape rather than checks.failure's bare id list. It does not include
checks.error (an ERROR is solver-level "could not determine," bucketed separately — see
failure_kind == "ERROR") or any cover-class property
(covers.unsatisfiable is that bucket's own list). This is why n_failed == len(checks.failure) on a
COMPLETED harness: n_failed is failed_properties.len(), whose membership is checks.failure's.

warnings is empty in the illustrative vacuity example. The synthetic fragment below shows the
shape of an untruncated warning, not a captured CBMC message or a warning-size measurement. The
warnings_truncated field and the truncated/original_chars pair are this proposal's additions, not
emitted by the PoC at 7b125f1b, which collects warning strings without truncation:

{
  "warnings": [
    {
      "message": "Example warning",
      "truncated": false,
      "original_chars": null
    }
  ],
  "warnings_truncated": 0
}

truncated/original_chars replace a [truncated; N chars total] suffix inside message: a
structural field a consumer checks without pattern-matching free text, avoiding the text parsing
this RFC argues against. original_chars is null when truncated is false
(nothing was cut). See “Statistics and truncation” below for what this field does and does not promise.

Statistics and truncation

Symex time, VCC counts and solver time exist only inside CBMC's free-text messages; extracting them requires
pattern-matching human-readable output, which causes the fragility this RFC is intended to prevent. benchcomp does
exactly this today; the right fix is structured data from CBMC, not more scraping. The warnings field
carries CBMC's messages as non-contractual free text, subject to the caps below: CBMC's --json-ui stream tags each
message with a messageType (e.g. "WARNING"), and this schema includes the WARNING-typed messages, for
example the SAT backend's warning: ignoring forall / warning: ignoring exists, emitted when it
cannot encode a quantifier with non-constant bounds. Later upstream
PR #4719, present at 10bc1ae04 but absent at
902daa525, explicitly parses these prefixes, counts the ignored quantifiers, and overrides the
property-derived result with failure and FailedProperties::Error. This internal interpretation does
not make warning text a versioned interface: an export consumer treats each message as opaque display text and uses Kani's
computed outcome instead of pattern-matching it. Two consequences:

• warnings is outside the schema_version compatibility guarantees. The field's presence and its
  [{ "message": …, "truncated": …, "original_chars": … }] shape are contractual; the contents of
  message are not, and must not be pattern-matched or assumed stable across versions.
• warnings is bounded, with explicit, structural truncation markers. The PoC collects warning
  strings without a length or count cap, so it places no fixed bound on their contribution to file
  size. This proposal caps each message at a fixed, implementation-defined length and truncates it
  on a character boundary, with the fact and extent carried as siblings truncated: bool and
  original_chars: integer | null (pre-truncation count, null
  exactly when truncated is false) rather than a suffix inside message. The per-harness warnings
  array is separately capped at a fixed count, with a sibling warnings_truncated integer per harness
  (0 when nothing was dropped) recording how many entries were omitted. A consumer can always tell
  "no more warnings" from "we stopped recording". These structural fields are schema-versioned; the
  message text is not.

Warning retention by outcome

Warnings do not depend on a property result array: CBMC may emit messages and then crash or be killed.
The PoC at 7b125f1b preserves collected warnings on its no-results crash/OOM path. Its timeout path
instead constructs a fresh result with no warnings. The export preserves whatever warnings the driver
retains, applying the same caps for every outcome; [] means none were retained, not proof that CBMC
emitted none.

3. Migration inventory

The inventory wording below is retained from the longer draft. Its shorthand for per-property detail
is inconsistent with that draft’s field tables: successful checks are counts, and other[] holds
only {id, status}. The RFC retains those field-table definitions unchanged.

• Shipped fields dropped or transformed in this shape — keep, drop, or make mandatory? Add --export-json for structured verification results #4472's
  document (create_metadata_json, create_harness_metadata_json, process_cbmc_results in
  kani-driver/src/frontend/schema_utils.rs) carries a number of fields this schema does not restore
  as-is. Grouped by proposed treatment:

  • Dropped, no successor field today: build_mode ("debug"/"release"); harnesses[].mangled_name
    (see “Why not mangled_name” in §2); the source range's end_line (only original_start_line
    survives, as harnesses[].line); goto_file (the generated modeling file path); per-check
    description/location for every property, not just the failed and other-bucketed ones (the
    shipped shape records full detail for every check; this schema records identities only for
    success/unreachable/undetermined/error/unknown, and full records only for
    failed_properties/unsupported_constructs/other[]); CBMC's OS banner (cbmc_metadata.os_info);
    and CBMC execution statistics
    (cbmc_stats: symex time, VCC counts, solver time — see "Why is CBMC statistics data excluded?" and
    the "Per-check timing" future-work item).

  • The effective --object-bits value stays an open question. It configures CBMC's pointer-object
    encoding and is useful verification provenance. The shipped writer already records it per harness
    at cbmc[].configuration.object_bits, resolving either Kani's default or the explicit
    --cbmc-args value. Its source is per-run state, so this schema could restore it under
    configuration or retain a per-harness field. On triage (--export-json: a failed, empty, or partial run can serialize as a clean pass #4731) a maintainer
    (feliperodri) classed it niche relative to is_bounded. Leaving it dropped is a provenance gap:
    adopting this RFC should file (or update) a tracking issue for its representation, resolved before
    or as part of stabilization.

  • The Cargo provenance project.workspace_root / output_dir, and harnesses[].file's base
    directory. harnesses[].file is written relative to the invocation directory
    (std::env::current_dir()), not any field this document carries; for a cargo kani run from the
    workspace root the two coincide, but for a standalone kani-driver invocation or a script that cds
    first they need not. Restoring workspace_root (or defining file as workspace-relative) makes
    file resolvable by a consumer that does not trust the launch directory. --target-dir does affect
    output_dir: Cargo builds derive it as <target-dir>/kani/<triple>/debug/deps (using Cargo's target
    directory when the flag is absent). It can stay dropped as an artifact-location field, but cannot
    be assumed to use the default path.

  • is_ctor_based is absent from HarnessMetadata and the shipped writer at 902daa525, but
    present in both at later upstream 10bc1ae04. There it records constructor-based generation or
    mined-invariant filtering: success covers only values admitted by that mechanism. This is a
    soundness-relevant restriction, independently of is_bounded. Its representation remains open in
    this draft, but support for exporting these harnesses must carry the restriction explicitly before
    stabilization; omitting it cannot justify reading their results as unrestricted proofs.

4. Configuration explanations and implementation inventory

configuration.checks.assertion_reach_checks. Whether Kani inserted reachability checks ahead of
ordinary assertions (true unless --no-assertion-reach-checks was passed). With reach-checks off, an
assertion made unreachable by a contradictory kani::assume is recorded in checks.success instead of
checks.unreachable, silently preventing the vacuity indication this schema provides; configuration
records exactly such toggles that change how a result must be read.

configuration.checks.ignore_global_asm and .extra_pointer_checks. Two more flags recorded for
the same reason. ignore_global_asm mirrors --ignore-global-asm: when true, Kani did not error on
global_asm!, so any behavior reachable only through that inline assembly is absent from the model and
a proof can pass vacuously with respect to its effects. extra_pointer_checks mirrors
--extra-pointer-checks: when true, Kani adds obligations for invalid pointers in relational
operations and pointer-arithmetic overflow, so two runs differing only in this flag check different
property sets, and checks.total/checks.success are not comparable between them.

configuration.checks.memory_safety, .overflow, .unwinding, and .undefined_function. The
remaining four checks bools, each mirroring a --no-*-checks flag (all default true; the field
name records the check being on, not the flag that turns it off):

• memory_safety mirrors --no-memory-safety-checks (and --no-default-checks, the whole group).
  false leaves out-of-bounds accesses and invalid-pointer dereferences unchecked; such a run can pass
  while containing the memory-safety bugs Kani is intended to detect.
• overflow mirrors --no-overflow-checks. false omits CBMC's NaN check and disables its
  division-by-zero check. It does not disable Rust/MIR arithmetic-overflow or integer
  division-by-zero assertions: Kani still compiles with -C overflow-checks=on and emits those MIR
  assertions (subject separately to prove_safety_only).
• unwinding mirrors --no-unwinding-checks. false stops CBMC asserting the loop/recursion bound
  covered every execution, so a bounded proof can silently miss behavior past the bound.
• undefined_function mirrors --no-undefined-function-checks. false skips Kani's generation of
  assert-false-assume-false bodies for undefined functions. Calls remain, with CBMC's default
  nondeterministic-return behavior; this does not model their possible side effects.

configuration.checks.assert_contracts and .prove_safety_only. These flags change generated
checks and assumptions, and therefore what a successful result establishes:

• assert_contracts mirrors --no-assert-contracts (true unless it was passed; it requires
  -Z function-contracts). When false, ordinary calls to contracted functions use
  ContractMode::Original: the original body executes and its contract instrumentation is omitted
  (kani_middle/transform/contracts.rs). The contracts are neither asserted nor assumed, so success
  does not establish those contract obligations. Explicit proof_for_contract checking and
  stub_verified replacement modes take precedence and retain their respective instrumentation.
• prove_safety_only mirrors --prove-safety-only (default false; requires -Z unstable-options).
  When true, codegen_assert_assume emits only an assumption for PropertyClass::Assertion. This
  includes ordinary user assertions and panic checks; success is conditional on those assumptions,
  not evidence that the converted assertions hold. Direct codegen_assert calls remain checks,
  including the internal CheckHook's Assertion-class properties. The conversion is specific to the
  code-generation path, not every property with that class.

All nine meet the same "changes which properties are generated, or what a status means" test.

Partial inventory of VerificationArgs (at 902daa525). Recorded directly: the
nine checks bools, coverage_enabled, and cbmc_args. Recorded elsewhere in the document, so not
duplicated here: -Z features that add or remove properties (uninit-checks, function-contracts,
loop-contracts, mem-predicates, quantifiers, stubbing) are visible by name in
enabled_unstable_features; --unwind/--default-unwind in per-harness resolved_unwind, resolved in
the order CLI --unwind > harness #[kani::unwind] > --default-unwind (is_bounded instead describes
autoharness argument generation);
--solver in the per-harness resolved_solver; --harness-timeout in harness_timeout_s and the
per-harness outcome.kind. This inventory is incomplete: --synthesize-loop-contracts transforms
each goto model before CBMC, while -Z restrict-vtable --no-restrict-vtable disables virtual-call
restriction without changing the recorded -Z feature set. Neither effective setting is represented
in the proposed fields. Their representation and the rest of the inventory must be resolved under
the policy before stabilization; cbmc_args does not capture Kani-generated options.

The proposed exclusion of --randomize-layout [seed] is a scope choice: it changes the program under
test (type layout), so its seed belongs in a future subject/provenance block. Presentation and
execution options also need individual treatment: regular/terse output controls rendering, but
--output-format=old uses mock results and is rejected with export. At 902daa525, --quiet
suppresses the failure exit in print_final_summary,
so a failed harness can be exported as failed while Kani exits 0. That is a driver bug, not a
different verification verdict. --jobs changes concurrency and can affect resource outcomes and
which results exist under fail-fast; --concrete-playback changes trace generation and formula
slicing as well as producing tests. These options cannot all be classified as affecting only presentation. Future flags
must be assessed under the same policy in the PR that adds them.

configuration.coverage_enabled. Mirrors --coverage (mandatory bool, default false). It
causes code_coverage (COVERED/UNCOVERED) properties to exist; these are excluded from checks,
covers, and n_properties, so it meets the configuration policy, and without it a consumer cannot
tell "no coverage properties in this schema yet" from "--coverage never passed." It sits alongside
checks.*, not nested under it.

The configuration policy itself remains in the RFC.

5. Deferred provenance and memory work

• Full tool & solver provenance beyond kani/rustc/cbmc. An earlier draft of this schema
  recorded goto_cc/goto_instrument/goto_synthesizer versions and a tools.solvers[] array of
  {name, version} per resolved solver (the shape the shipped Add --export-json for structured verification results #4472 writer already emits), plus a
  proposed source: "builtin"|"external" discriminator (this schema's own addition, not part of Add --export-json for structured verification results #4472)
  to disambiguate a null version. Cut from v1 to keep it to the core (per
  model-checking/kani#4731): probing the extra
  tools' and external solvers' --version spawns a process per tool beyond the probes v1 already needs,
  and the solver CBMC ran with is already recoverable per harness from harnesses[].resolved_solver. A
  follow-up can restore the fuller tools.solvers[] block if a consumer needs the solver binary
  versions. File a tracking issue on adoption.
• Host machine environment (machine). An earlier draft carried machine.cpu_count,
  .total_memory_bytes, .memory_limit_bytes, .os, .arch. Cut from v1: environment metadata that
  helps triage performance/OOM but is not needed to reproduce a verdict. A follow-up can reintroduce a
  machine block if performance-oriented consumers ask for it. File a tracking issue on adoption.
• Per-check timing and resource data. Used elsewhere (GNATprove reports per-obligation
  prover data), but not available from CBMC's structured output today.
• A machine-reproducible counterexample. --concrete-playback already derives a concrete value
  vector; exposing it would let a consumer reproduce a failure without modifying source.
• A finer failure classification. Kani computes whether a failure involved unwinding assertions
  or reachable undefined functions, then collapses them; separating them would let a consumer tell
  "raise --unwind and retry" from "fix the code".
• A harness-level triviality signal, aggregating what RFC 0003 already identifies as the
  vacuity concern.
• Aggregate coverage, deferring to kani-cov and RFC 0011.
• The contract trust chain. A harness using stub_verified is sound only if the contract's own
  proof passed. Kani already enforces at compile time that such a harness exists; because this schema
  records both relationships, a consumer can check the run-time condition itself today, and Kani could report the
  resolved status later.
• Per-harness peak memory. A getrusage(RUSAGE_CHILDREN)-based approach was prototyped and rejected:
  ru_maxrss is a process-wide running maximum, not a per-child figure, so the result is
  order-dependent (only a harness whose peak memory exceeds that of every earlier harness gets a value; a later one with
  a lower peak reads null even under memory pressure) and is not attempted under --jobs, where the counter is shared
  across siblings. An accurate figure needs per-child accounting (e.g. wait4()-based rusage per child,
  or a per-child cgroup with its own memory.peak), which this schema does not attempt. Kani infers OOM
  from the CBMC child's status 137 when no property result array is available, and this schema
  exposes that inference as outcome.kind == "OUT_OF_MEMORY". Kani normally exits 1 for the failed
  harness, not 137; at 902daa525, the --quiet bug can instead leave its exit code at 0.

6. Failure and completeness explanations

Failure scenarios.

• The output path is not writable → reported as an error with a non-zero exit, never silently ignored.
  The verification verdict is computed independently and never rewritten by an export problem. The
  up-front marker write fails before verification starts; the terminal export runs after the harness
  verdicts but before the SARIF artifact and final summary line, so a terminal export failure aborts
  those remaining steps. (Whether it should suppress the SARIF write is an implementation question, not
  settled here.)
• Any tools.* version cannot be determined → that field is null, never guessed; see "Tool
  provenance" above.
• A harness times out, is OOM-killed, or CBMC crashes on it → that harness's outcome.kind
  (TIMEOUT/OUT_OF_MEMORY/CRASHED) records it and the file is still written. Run completeness is
  verdict-independent: as long as every selected harness has an entry in the terminal document,
  run_state is COMPLETE (a suite where every harness times out is complete accounting for unsuccessful verification
  attempts). PARTIAL means the terminal document lacks some selected harness results; INCOMPLETE
  means only the marker was published.
• Kani itself crashes (a kani-compiler ICE, a panic in kani-driver, a SIGKILL) → no terminal
  document is written: the single terminal write happens once at the very end (verify_project), and any
  hard error before it unwinds past it. There is no run-level "CRASHED" value; all that remains is a
  stale INCOMPLETE marker (or, if the crash preceded it, whatever file already existed). See "How
  run_state and outcome.kind co-occur" below.
• The --export-json path already holds a file → it is overwritten up front with an atomic
  run_state: "INCOMPLETE" marker once harness verification begins (after the crate is built), so an
  earlier run's results cannot be misread as this run's, and a run that terminates after that without finishing leaves a file that
  records that it did not finish (replacing an earlier delete-up-front design; see the RFC’s completeness
  contract and open question).
• The parent directory does not exist → it is created (create_dir_all), matching --sarif. A path
  that is itself an existing directory fails today only when the write is attempted (the same-directory
  temp write cannot be created inside a file-shaped target); adopting this RFC moves that to the
  argument-parse-time rejection proposed under Interaction with other flags, so the failure occurs
  before any verification work, as for --sarif. The shipped difference is an accident of
  implementation order, not intentional.

How run_state and outcome.kind co-occur. outcome is meaningful only once Kani reaches a
terminal write, and at run level its kind has exactly one value: COMPLETED. The marker
(run_state == "INCOMPLETE") is written before that and carries no outcome. A run-level
outcome.kind == "CRASHED" does not exist (see the crash scenario above); what a consumer observes
instead is a stale INCOMPLETE marker, or a missing file. The crash indication is that staleness rather
than a field value. Every producible combination:

run_state	outcome
INCOMPLETE (marker)	absent
COMPLETE	{"kind": "COMPLETED"}
PARTIAL	{"kind": "COMPLETED"}
NO_HARNESSES_SELECTED	{"kind": "COMPLETED"}

Per-harness outcome.kind == "CRASHED" is unaffected and remains possible: the run can finish, reach
its terminal write, and report that CBMC crashed on one harness. This describes one harness in a
completed document, distinct from Kani never reaching the write.

NO_HARNESSES_SELECTED means exactly one thing: an unfiltered run of a selected project or workspace
with no selectable harness (no #[kani::proof], or under autoharness no eligible function). It
cannot arise from a --harness filter: a filter set that matches nothing — and, with --exact, any single filter
that matches nothing — is rejected at harness selection (no_harness_match_error in
kani-driver/src/metadata.rs, since #4743) with a non-zero exit. Harness selection precedes the
INCOMPLETE marker write and every export, so that case produces no document at all, not a
terminal document with a non-empty requested_filters. Hence in a NO_HARNESSES_SELECTED document
harness_selection.requested_filters == [], unmatched_filters == [], and matched_count == 0.
unmatched_filters is non-empty only in a COMPLETE/PARTIAL document written without --exact, where
at least one filter matched and the named ones did not.

Cover-only vacuity is not detected by this schema alone. The RFC’s normative and advisory
vacuity predicates read only checks.*; an unreachable cover is recorded in covers.unreachable and
satisfies neither. A consumer wanting the corresponding indication for covers should additionally apply covers.total > 0 && covers.unreachable.len() == covers.total per harness, since this schema does not apply it for them.

null always means not measured or not applicable, never a guess, and is always distinguishable
from 0, false, and [].

7. Casing and requested versus resolved values

Casing. The file mixes three conventions, and one rule explains all three: a value keeps the
serialization of the Rust type it comes from, and this schema does not fork types to re-case them.

• snake_case keys, because the schema reuses kani_metadata and cbmc_output_parser types directly
  (HarnessAttributes, AssignsContract, CheckStatus); re-casing would fork those types, recreate the
  duplication problem in #3541, or break existing
  .kani-metadata.json consumers. Those three already derive Serialize; but Property, PropertyId,
  and SourceLocation derive only Deserialize (never serialized out), so
  failed_properties[]/unsupported_constructs[]/checks.other[]/covers.other[] are purpose-built
  export structs rather than a direct embedding of Property.
• SCREAMING_SNAKE_CASE enum values (outcome.kind, verdict, failure_kind, run_state, every
  status), mirroring the reused CBMC-status types (CheckStatus, FailedProperties); the new enums
  (Outcome, verdict, run_state) use it too, so a consumer sees one value convention across the file.
  (Multi-word values like NO_HARNESSES_SELECTED need an explicit SCREAMING_SNAKE_CASE rename, since
  CheckStatus's UPPERCASE coincides with it only for single-word variants.)
• PascalCase, object-shaped, for the two embedded kani_metadata attribute enums below, which keep
  their own serde derivation untouched for the same no-forking reason.

Fields that are not always strings. Two reused kani_metadata enums have non-unit variants and so
serialize as objects, not strings:

• harnesses[].attributes.kind is "Proof" or "Test", but {"ProofForContract": {"target_fn": "…"}}
  for a contract-proof harness.
• harnesses[].attributes.solver is "Cadical", "Z3", etc. for a named solver, but {"Binary": "…"}
  for a custom solver path.

These are the requested attributes, carried verbatim from .kani-metadata.json; the resolved
counterparts (resolved_solver, resolved_unwind) are plain scalars (a string or number, or null),
never the object forms above.

Reconciling the two solver spellings. attributes.solver is the requested value in CbmcSolver's
PascalCase ("Cadical", or {"Binary": "<path>"} for a custom solver); resolved_solver is the
lowercase built-in name or custom binary path CBMC actually ran with. Effective precedence is the last
solver-selecting --cbmc-args override > CLI --solver > harness attribute > default: Kani appends
cbmc_args after its own solver flags. Bare --smt2 leaves the choice to CBMC and yields null.
Compare attributes.solver against resolved_solver for "asked for" vs "ran".

This proposal follows kani list by recording tool version and schema version in separate
fields; see the RFC’s Compatibility policy.

[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.

[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.

[Copilot]

🟡 Changes recommended

The schema omits result-altering flags and contains inconsistent stabilization and empty-selection requirements.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Defines an unstable JSON schema for machine-readable Kani verification results, including harness outcomes, vacuity signals, provenance, and completeness semantics.

Changes:

• Specifies the --export-json schema and compatibility policy.
• Documents result interpretation, failure modes, and future work.
• Adds RFC navigation entries.

File summaries

File	Description
rfc/src/SUMMARY.md	Adds RFC 0014 and 0015 links.
rfc/src/rfcs/0015-export-json.md	Defines the structured verification-results RFC.

Review details

• Files reviewed: 2/2 changed files
• Comments generated: 3
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

@ivmat can you address the Copilot comments?

[ivmat]

@feliperodri this revision applies the requested changes and includes a source-accuracy pass, with statements re-verified against source. the rfc has been tightened with longer explanations in b part of the pr body